mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ h.desc s ∘ₗ solution.π = s.π

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ solution.postcomp (h.desc s) = s

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
⊢ (ofQuotient relations).fromQuotient = LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ solution.postcomp (solution.fromQuotient ∘ₗ h.down.desc (ofQuotient relations)) = solution.postcomp LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ h.down.desc (ofQuotient relations) ∘ₗ solution.fromQuotient = LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this✝ : Fintype κ
w : κ → R
hw : ∑ i, w i • ∑ j, A i j • v j = 0
this : w = 0
⊢ ∀ (i : κ), w i = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ e.toMatrix (v + w) i j = (e.toMatrix v + e.toMatrix w) i j

Tactic:
Matrix.add_apply,

Goal state after:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ e.toMatrix (v + w) i j = e.toMatrix v i j + e.toMatrix w i j
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_1.hx
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := ⋯
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ u ∈ Set.range ⇑f.toHomUnits

Tactic:
simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) → ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
⊢ (a • 1).det = 1

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
ext m; exact map_apply_ι _ m

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ σ₂ (Pi.single j 1 x✝¹) •> σ₁ (Pi.single i 1 x✝³) •> f x✝³ x✝¹ =
    (if i = x✝³ then 1 else 0) •> (if j = x✝¹ then 1 else 0) •> f x✝³ x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
⊢ (f 0) GradedMonoid.GOne.one = 1

Tactic:
exact hone

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) (x✝¹ + x✝)) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)

Tactic:
decompose_add,

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) x✝¹ + (decompose 𝒜) x✝) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = ↑(r x✝¹) * ↑(r' x✝)

Tactic:
subst h
    rw [of_eq_same]
    rfl

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
x : ι × ι
hx : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = k}
⊢ x.1 < m ∨ x.2 < n

Tactic:
by
    by_contra! ⟨hm, hn⟩
    obtain rfl : x.1 + x.2 = k := by simp_all
    apply lt_irrefl (m + n) <| lt_of_le_of_lt (by gcongr) hk

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
⊢ involute x = x

Tactic:
induction x, h using even_induction with
  | algebraMap r => exact AlgHom.commutes _ _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldr (fun m n ↦ (f m) n) n l

Tactic:
by
  induction l with
  | nil => rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
  | cons hd tl ih => rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
⊢ w j * (w j * ⅟2 (Q (v j + v j) - Q (v j) - Q (v j))) = ⅟2 (Q (v j + v j) - Q (v j) - Q (v j)) * (w j * w j)

Tactic:
half_moduleEnd_apply_eq_half_smul

Goal state after:
ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
⊢ w j * (w j * ⅟2 • (Q (v j + v j) - Q (v j) - Q (v j))) = ⅟2 • (Q (v j + v j) - Q (v j) - Q (v j)) * (w j * w j)
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
⊢ ∀ (x y : MultilinearMap R N M₂), (x + y).currySum = x.currySum + y.currySum

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
⊢ ∀ (m : R) (x : MultilinearMap R N M₂), (m • x).currySum = (RingHom.id R) m • x.currySum

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
⊢ x = 0 ∧ r = 0

Tactic:
let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
    have : IsCentralScalar R M := ⟨fun r m => rfl⟩
    have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _
    rw [h, AlgHom.commutes] at hf0
    have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
    exact this.symm.imp_left Eq.symm

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ f (x.pred hx).succ = f (y.pred ⋯).succ

Tactic:
simp only [Fin.succ_pred]

Goal state after:
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ f x = f y
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
⊢ ∃ a, f a = y
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r • (M.mk F ⟨i, x⟩ + M.mk F ⟨j, y⟩) = M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩

Tactic:
colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
      (IsFiltered.rightToMax i j),

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r •
      M.mk F
        ⟨IsFiltered.max i j,
          (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd + (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          r • (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩

Tactic:
colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
      (IsFiltered.rightToMax i j),

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          r • (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F
      ⟨IsFiltered.max i j,
        (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, r • ⟨i, x⟩.snd⟩.snd +
          (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, r • ⟨j, y⟩.snd⟩.snd⟩
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
inst✝³ : DecidableEq ι
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
x y : M
this : s.var (update m i x) + s.var (update m i y) = s.var (update m i (x + y))
⊢ s.var (update m i (x + y)) = s.var (update m i x) + s.var (update m i y)

Tactic:
convert! this.symm

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
N✝ : Type ?u.42
inst✝¹ : AddCommGroup N✝
inst✝ : Module R N✝
s : (relations R (Fin n) M).Solution N✝
⊢ (relationsSolutionEquiv.symm (ιMulti R n)).postcomp
      (ExteriorAlgebra.liftAlternating (update 0 n (relationsSolutionEquiv s)) ∘ₗ (⋀[R]^n M).subtype) =
    s

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : ↑(powersetCard I n)
⊢ (map n f) (ιMulti_family R n v s) = ιMulti_family R n (⇑f ∘ v) s

Tactic:
by
  simp only [ιMulti_family, map, alternatingMapLinearEquiv_apply_ιMulti]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) ∘ₗ
      { toFun := fun r ↦ r • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim, map_add' := ⋯, map_smul' := ⋯ } =
    LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ { toFun := fun r ↦ r • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) =
    LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ↑(zeroEquiv R N) ∘ₗ map 0 f = ↑(zeroEquiv R M)

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ (alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) ∘ₗ
      have h := ⋯;
      { toFun := fun m ↦ (ιMulti R 1) fun x ↦ m, map_add' := ⋯, map_smul' := ⋯ }) =
    LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ (have h := ⋯;
      { toFun := fun m ↦ (ιMulti R 1) fun x ↦ m, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) =
    LinearMap.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ↑(oneEquiv R N) ∘ₗ map 1 f = f ∘ₗ ↑(oneEquiv R M)

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
inst✝⁶ : MonoidalCategory D✝
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : MonoidalCategory D
inst✝¹ : MonoidalCategory E
L : D ⥤ E
inst✝ : L.OplaxMonoidal
⊢ ∀ (X : C ⥤ D),
    (λ_ (((Functor.whiskeringRight C D E).obj L).obj X)).inv =
      ((Functor.whiskeringRight C D E).obj L).map (λ_ X).inv ≫
        { app := fun X_1 ↦ δ L ((𝟙_ (C ⥤ D)).obj X_1) (X.obj X_1), naturality := ⋯ } ≫
          { app := fun X ↦ η L, naturality := ⋯ } ▷ ((Functor.whiskeringRight C D E).obj L).obj X

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
inst✝⁶ : MonoidalCategory D✝
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : MonoidalCategory D
inst✝¹ : MonoidalCategory E
L : D ⥤ E
inst✝ : L.OplaxMonoidal
⊢ ∀ (X : C ⥤ D),
    (ρ_ (((Functor.whiskeringRight C D E).obj L).obj X)).inv =
      ((Functor.whiskeringRight C D E).obj L).map (ρ_ X).inv ≫
        { app := fun X_1 ↦ δ L (X.obj X_1) ((𝟙_ (C ⥤ D)).obj X_1), naturality := ⋯ } ≫
          ((Functor.whiskeringRight C D E).obj L).obj X ◁ { app := fun X ↦ η L, naturality := ⋯ }

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j : C
⊢ ∀ (j₁ j₂ : C) (x : j₁ ⟶ j₂),
    (ConcreteCategory.hom (s.ι.app j₁)) PUnit.unit = (ConcreteCategory.hom (s.ι.app j₂)) PUnit.unit

Tactic:
intro X Y f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (s.ι.app X)) PUnit.unit = (ConcreteCategory.hom (s.ι.app Y)) PUnit.unit
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
m : (pUnitCocone C).pt ⟶ s.pt
h : ∀ (j : C), (pUnitCocone C).ι.app j ≫ m = s.ι.app j
⊢ (ConcreteCategory.hom m).toFun PUnit.unit = (ConcreteCategory.hom (s.ι.app Classical.ofNonempty)).toFun PUnit.unit

Tactic:
simp [← h Classical.ofNonempty]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
refine ⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
    F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ s ≫ IsFiltered.coeqHom s s' = s' ≫ IsFiltered.coeqHom s s'

Tactic:
IsFiltered.coeq_condition

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ s' ≫ IsFiltered.coeqHom s s' = s' ≫ IsFiltered.coeqHom s s'