update

forked-from-1kasper · Nov 8, 2022 · 5e93d37 · 5e93d37
1 parent 5e5162d
commit 5e93d37
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 7 deletions.
diff --git a/GroundZero/Algebra/Basic.lean b/GroundZero/Algebra/Basic.lean
@@ -16,9 +16,6 @@ namespace GroundZero.Algebra
   hott def zeroeqv {A : Type u} (H : hset A) : 0-Type :=
   ⟨A, zeroEqvSet.left H⟩
 
-  macro "propauto" : tactic =>
-    `(repeat { apply piProp; intro }; apply p)
-
   def algop (deg : ℕ) (A : Type u) :=
   vect A deg → A
 

diff --git a/GroundZero/Algebra/Orgraph.lean b/GroundZero/Algebra/Orgraph.lean
@@ -259,15 +259,15 @@ namespace GroundZero.Algebra
     @minorant T.κ φ x → @majorant T.κ (@Neg T.τ φ) (T.τ.neg x) :=
   begin
     intros H x p; apply invMinusSign;
-    apply Equiv.transport (λ y, T.ρ y (-x)); symmetry;
+    apply Equiv.transport (λ y, T.ρ y (T.τ.neg x)); symmetry;
     apply @Group.invInv T.τ⁺; apply H; exact p
   end
 
   noncomputable hott def Neg.negMajorant {T : Overring} [orfield T] {φ : T.subset} (x : T.carrier) :
     @minorant T.κ (@Neg T.τ φ) x → @Algebra.majorant T.κ φ (T.τ.neg x) :=
   begin
     intro H; intros x p; apply invMinusSign;
-    apply Equiv.transport (λ y, T.ρ y (-x)); symmetry;
+    apply Equiv.transport (λ y, T.ρ y (T.τ.neg x)); symmetry;
     apply @Group.invInv T.τ⁺; apply H; apply Equiv.transport (· ∈ φ);
     symmetry; apply @Group.invInv T.τ⁺; exact p
   end
@@ -276,15 +276,15 @@ namespace GroundZero.Algebra
     @Algebra.majorant T.κ φ x → @Algebra.minorant T.κ (@Neg T.τ φ) (T.τ.neg x) :=
   begin
     intro H x p; apply invMinusSign;
-    apply Equiv.transport (T.ρ (-x)); symmetry;
+    apply Equiv.transport (T.ρ (T.τ.neg x)); symmetry;
     apply @Group.invInv T.τ⁺; apply H; exact p
   end
 
   noncomputable hott def Neg.negMinorant {T : Overring} [orfield T] {φ : T.subset} (x : T.carrier) :
     @Algebra.majorant T.κ (@Neg T.τ φ) x → @Algebra.minorant T.κ φ (T.τ.neg x) :=
   begin
     intro H x p; apply invMinusSign;
-    apply Equiv.transport (T.ρ (-x)); symmetry;
+    apply Equiv.transport (T.ρ (T.τ.neg x)); symmetry;
     apply @Group.invInv T.τ⁺; apply H; apply Equiv.transport (· ∈ φ);
     symmetry; apply @Group.invInv T.τ⁺; exact p
   end