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
⊢ solution.IsPresentation ↔
    Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
← injective_fromQuotient_iff_ker_π_eq_span,

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.IsPresentation ↔ Submodule.span A (Set.range solution.var) = ⊤ ∧ Function.Injective ⇑solution.fromQuotient
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case left
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤

Tactic:
assumption

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

Goal state before:
pp: case right
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ∃ a, det a = r

Tactic:
refine ⟨⟨diagonal fun j ↦ if j = i then r else 1, diagonal fun j ↦ if j = i then r⁻¹.1 else 1,
    ?_, ?_⟩, by simp [det]⟩
  <;> simp only [diagonal_mul_diagonal, mul_ite, ite_mul, Units.mul_inv, one_mul, mul_one,
      diagonal_eq_one]

Goal state after:
case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then 1 else ↑r⁻¹ else if i_1 = i then ↑r else 1) = 1

case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then ↑r⁻¹ * ↑r else ↑r else if i_1 = i then ↑r⁻¹ else 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := ⋯
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ coeMonoidHom ⟨diagonal D, hD⟩ =
    coeMonoidHom ({i | i ≠ i₀}.noncommProd (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) ⋯)

Tactic:
rw [Finset.map_noncommProd]

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ coeMonoidHom ⟨diagonal D, hD⟩ =
    {i | i ≠ i₀}.noncommProd (fun i ↦ coeMonoidHom (if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1)) ⋯
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case succ
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ 1 * 1 + ↑n * 1 = ↑n + 1

Tactic:
rw [mul_one, mul_one, add_comm]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
a : R
x y : M
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y

Tactic:
by
  obtain ⟨B, h⟩ := Q.exists_companion
  simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]

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
i j : ι
ai : A i
aj : A j
⊢ F ((of A (i + j)) (GradedMonoid.GMul.mul ai aj)) = F ((of A i) ai) * F ((of A j) aj)

Tactic:
← F.map_mul (of A i ai),

Goal state after:
ι : 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
i j : ι
ai : A i
aj : A j
⊢ F ((of A (i + j)) (GradedMonoid.GMul.mul ai aj)) = F ((of A i) ai * (of A j) aj)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons.e_a.e_a.a
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
i : ι
hi : i ∈ s
⊢ polar (⇑Q) (f a) (f i) = if ¬a = i then polar (⇑Q) (f a) (f i) else 0

Tactic:
rw [if_pos (ne_of_mem_of_not_mem hi ha).symm]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (proj 𝒜 i) ((decompose 𝒜).symm a) = (decompose 𝒜).symm ((of (fun i ↦ ↥(𝒜 i)) i) (a i))

Tactic:
by
  rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]

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

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
⊢ 2 • (associatedHom S) Q = Q.polarBilin

Tactic:
by
  ext
  dsimp [associated_apply]
  rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]

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

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra S R
inst✝⁴ : Module S N
inst✝³ : IsScalarTower S R N
inst✝² : Invertible 2
Q : QuadraticMap R M N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N' →ₗ[R] M
x✝¹ x✝ : N'
⊢ (((associatedHom S) (Q.comp f)) x✝¹) x✝ = ((LinearMap.compl₁₂ ((associatedHom S) Q) f f) x✝¹) x✝

Tactic:
simp only [associated_apply, comp_apply, map_add, LinearMap.compl₁₂_apply]

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

Goal state before:
pp: case h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ∀ x ∈ DFinsupp.support r', ¬i + x = n

Tactic:
exact fun x _ H => h ((self_le_add_right i x).trans_eq H)

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✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ s.prod n = 0

Tactic:
have := listProd_apply_eq_zero (l := s.toList) (by simpa using hs)
    (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
this : s.toList.prod n = 0
⊢ s.prod n = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr.refine_1.refine_1
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
hij : 0 ≠ 0
⊢ Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) 0 0

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Goal state after:
case succ.inr.refine_1.refine_1
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
hij : 0 ≠ 0
⊢ (B x) x = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr.refine_1.refine_2
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j✝ i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
⊢ Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j.succ 0

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Goal state after:
case succ.inr.refine_1.refine_2
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j✝ i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
⊢ (B ↑(v' j)) x = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr.refine_2.refine_1
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i✝ : Fin (d + 1)
i : Fin d
hij : 0 ≠ i.succ
⊢ Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) 0 i.succ

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Goal state after:
case succ.inr.refine_2.refine_1
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i✝ : Fin (d + 1)
i : Fin d
hij : 0 ≠ i.succ
⊢ (B x) ↑(v' i) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) (m * x) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i.succ) ⟨m * x, ⋯⟩

Tactic:
obtain ⟨_, rfl⟩ := hm
      rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
      refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_) <;>
        dsimp only [GradedMonoid.mk, Subtype.coe_mk]
      · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
      rfl

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

Goal state before:
pp: case succ.inr.refine_2.refine_2
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j✝ i✝ : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j.succ i.succ

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Goal state after:
case succ.inr.refine_2.refine_2
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j✝ i✝ : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ (B ↑(v' j)) ↑(v' i) = 0
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
b : β
⊢ b ∈ map n f s ↔ b ∈ ⇑f '' ↑s

Tactic:
simp [map]

Goal state after:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
b : β
⊢ (∃ a ∈ ↑s, f a = b) ↔ ∃ x ∈ s, f x = b
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

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

Tactic:
rw [map_zero, map_zero]

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

Goal state before:
pp: case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn

Goal state after:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
⊢ (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod +
      (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod =
    0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (liftAlternating f) ((ι R) m * x) = (liftAlternating fun i ↦ (f i.succ).curryLeft m) x

Tactic:
by
  dsimp [liftAlternating]
  rw [foldl_mul, foldl_ι]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ LinearIndependent R u

Tactic:
by
  rw [linearIndependent_sum]
  refine ⟨?_, LinearIndependent.of_comp S.g.hom hw, disjoint_span_sum hS hw huv⟩
  rw [huv, LinearMap.linearIndependent_iff S.f.hom]; swap
  · rw [LinearMap.ker_eq_bot, ← mono_iff_injective]
    infer_instance
  exact hv

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
x✝¹ : AddCommGroup N
x✝ : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
⊢ f = f'

Tactic:
Submodule.linearMap_eq_iff_of_span_eq_top _ _ (ιMulti_span R n M)

Goal state after:
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
x✝¹ : AddCommGroup N
x✝ : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
⊢ ∀ (s : ↑(range ⇑(ιMulti R n))), f ↑s = f' ↑s
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
f : M [⋀^Fin n]→ₗ[R] N
⊢ (alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n) = f

Tactic:
obtain ⟨φ, rfl⟩ := alternatingMapLinearEquiv.symm.surjective f

Goal state after:
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
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (alternatingMapLinearEquiv (alternatingMapLinearEquiv.symm φ)).compAlternatingMap (ιMulti R n) =
    alternatingMapLinearEquiv.symm φ
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case h
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
⊢ ExteriorAlgebra.ιMulti_family R n v ⟨Finset.image α Finset.univ, α_card⟩ =
    (ExteriorAlgebra.ιMulti R n)
      ((v ∘ α) ∘
        ⇑(((Finset.image α Finset.univ).orderIsoOfFin α_card).trans
            ((Equiv.setCongr ⋯).trans (Equiv.ofInjective α α_inj).symm)))

Tactic:
ExteriorAlgebra.ιMulti_family,

Goal state after:
case h
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ ⇑(ofFinEmbEquiv.symm ⟨Finset.image α Finset.univ, α_card⟩)) =
    (ExteriorAlgebra.ιMulti R n)
      ((v ∘ α) ∘
        ⇑(((Finset.image α Finset.univ).orderIsoOfFin α_card).trans
            ((Equiv.setCongr ⋯).trans (Equiv.ofInjective α α_inj).symm)))
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
⊢ IsIso f₂

Tactic:
have : Function.Bijective f₂.hom := by
    rw [← IsLocalizedModule.linearEquiv_of_isLocalizedModule_comp S f₁.hom f₂.hom]
    exact (IsLocalizedModule.linearEquiv ..).bijective
  simpa [ConcreteCategory.isIso_iff_bijective]

Goal state after: