mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
⊢ ∃ e, (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range = (↑e).graph

Tactic:
by
  -- apply add-group result
  obtain ⟨(e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd), he⟩ :=
    L.toAddSubgroup.goursat_surjective hL₁ hL₂
  -- check R-linearity of the map
  have (r : R) (x : M ⧸ L.goursatFst) : e (r • x) = r • e x := by
    change (r • x, r • e x) ∈ e.toAddMonoidHom.graph
    rw [← he, ← Prod.smul_mk]
    have : (x, e x) ∈ e.toAddMonoidHom.graph := rfl
    rw [← he, AddMonoidHom.mem_range] at this
    rcases this with ⟨⟨l, hl⟩, hl'⟩
    use ⟨r • l, L.smul_mem r hl⟩
    rw [← hl']
    rfl
  -- define the map as an R-linear equiv
  use { e with map_smul' := this }
  rw [← toAddSubgroup_injective.eq_iff]
  convert! he using 1
  ext v
  rw [mem_toAddSubgroup, mem_graph_iff, Eq.comm]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i

Tactic:
let v' (i : ι) : I := ⟨v i, hv.linearIndepOn_id.subset_extend _ <| mem_range_self i⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ ⋯.choose * a hj.choose = g i

Tactic:
mul_comm

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ a hj.choose * ⋯.choose = g i
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
| g i

Tactic:
← hj.choose_spec,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
| g (f hj.choose)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ (∏ x ∈ {x | ∃ j, f j = x}.attach, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index) *
      Nat.card R ^ {x | ¬∃ j, f j = x}.card =
    Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
mul_comm

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ Nat.card R ^ {x | ¬∃ j, f j = x}.card *
      ∏ x ∈ {x | ∃ j, f j = x}.attach, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : i < a
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
Fin.succAbove_succ_of_lt _ _ h,

Goal state after:
case neg.inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : i < a
⊢ M a.succ b = M (i.castSucc.succAbove a) b
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι

Tactic:
rw [snf.toAddSubgroup_index_eq_ite]

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ (if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0) ≠ 0 ↔
    n = Fintype.card ι
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᴴ * Aᴴᴴ = ↑(Fintype.card n) • 1

Tactic:
by simpa using hA.conjTranspose_mul

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.det ≠ 0

Tactic:
← Matrix.det_transpose

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.transpose.det ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B (a, b) (c, d) = 0

Tactic:
simp [hA hac]

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

Goal state before:
pp: case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x, c * M (x✝ x) x = c ^ Fintype.card n * ∏ i, M (x✝ i) i

Tactic:
mul_comm

Goal state after:
case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x, c * M (x✝ x) x = (∏ i, M (x✝ i) i) * c ^ Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ detp s Ai = ∑ j, detp (-s) (Aj j) * A.col (g j) i + detp s D * A.col j₀ i

Tactic:
mul_comm

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ detp s Ai = ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
b : (i : ι) → Basis (κ i) R (M i)
x : (i : ι) → M i
p : (i : ι) → κ i
⊢ ((Finsupp.basisSingleOne.map
            (((PiTensorProduct.congr fun i ↦ (b i).repr).trans ofFinsuppEquiv).trans
                (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) ↑(constantBaseRingEquiv ι R))).symm).repr
        ((tprod R) x))
      p =
    ∏ i, ((b i).repr (x i)) (p i)

Tactic:
Subsingleton.elim (Fintype.ofFinite ι) ‹_›

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
b : (i : ι) → Basis (κ i) R (M i)
x : (i : ι) → M i
p : (i : ι) → κ i
⊢ ((Finsupp.basisSingleOne.map
            (((PiTensorProduct.congr fun i ↦ (b i).repr).trans ofFinsuppEquiv).trans
                (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) ↑(constantBaseRingEquiv ι R))).symm).repr
        ((tprod R) x))
      p =
    ∏ i, ((b i).repr (x i)) (p i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
f : (i : ι) → Dual R (M i)
m : (i : ι) → M i
⊢ ((compRight R (constantBaseRingEquiv ι R).toLinearMap ∘ₗ piTensorHomMap) ((tprod R) fun i ↦ f i))
      (⨂ₜ[R] (i : ι), m i) =
    ∏ i, (f i) (m i)

Tactic:
Subsingleton.elim (Fintype.ofFinite ι) ‹_›

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
f : (i : ι) → Dual R (M i)
m : (i : ι) → M i
⊢ ((compRight R (constantBaseRingEquiv ι R).toLinearMap ∘ₗ piTensorHomMap) ((tprod R) fun i ↦ f i))
      (⨂ₜ[R] (i : ι), m i) =
    ∏ i, (f i) (m i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case succ.e_f.hg
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) := ⋯
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
g₀ : γ i₀
⊢ ∀ (i : ↑{i₀}ᶜ), Submodule.span R (Set.range fun j ↦ g j) = ⊤

Tactic:
intro

Goal state after:
case succ.e_f.hg
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
g₀ : γ i₀
i✝ : ↑{i₀}ᶜ
⊢ Submodule.span R (Set.range fun j ↦ g j) = ⊤
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
⊢ (Algebra.ofId R (⨂[R] (x : ι), R)).comp (AlgHom.ofLinearMap toFun ⋯ ⋯) = AlgHom.id R (⨂[R] (x : ι), R)

Tactic:
by classical ext

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
hF : 4 ≤ Nat.card F
this : Finite F
⊢ IsCyclic Fˣ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
⊢ A • v = v

Tactic:
(Mathlib.Tactic.setTactic
 "set"
 []
 (Mathlib.Tactic.setArgsRest
  (Lean.binderIdent `L)
  [":"
   (Term.app
    `Submodule
    [`F (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.arrow `ι "→" `F) ")")])]
  ":="
  (Term.app
   `Submodule.span
   [`F
    (choice
     («term{_}» "{" [`v] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `v []) [])])
      (Term.optEllipsis [])
      []
      "}"))])
  []))

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
⊢ A • v = v
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Subsingleton (Module.Free.ChooseBasisIndex R V)
⊢ Subsingleton ↥(Subgroup.center (Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R))

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ QuadraticMap R (M ⧸ N) P

Tactic:
refine QuadraticMap.mk (Quotient.lift Q <| by exact lift_aux hN)
    (fun a m ↦ m.inductionOn (Q.map_smul a)) ?_

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∃ B, ∀ (x y : M ⧸ N), Quotient.lift ⇑Q ⋯ (x + y) = Quotient.lift ⇑Q ⋯ x + Quotient.lift ⇑Q ⋯ y + (B x) y
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ N ≤ Q.radical → ∃ Q', Q'.comp N.mkQ = Q

pp: case mpr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ (∃ Q', Q'.comp N.mkQ = Q) → N ≤ Q.radical

Tactic:
· exact fun hN ↦ ⟨Q.lift N hN, rfl⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ (∃ Q', Q'.comp N.mkQ = Q) → N ≤ Q.radical
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
m : ι
hm : P.root m = P.root ↑i + P.root ↑j
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ m →
      (if P.root b_1 = P.root ↑i + P.root ↑j ∧ P.root ↑i = P.root b_1 - P.root ↑j then ↑(chainTopCoeff (↑j) b_1) + 1
        else 0) =
        0

Tactic:
rintro x - hx; simp [← hm, hx]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ (-ω b * ⁅e j, f i⁆) (Sum.inr k) (Sum.inr ↑i) = 0 (Sum.inr k)

Tactic:
← (-ω b * ⁅e j, f i⁆).transpose_apply,

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ (-ω b * ⁅e j, f i⁆)ᵀ (Sum.inr ↑i) (Sum.inr k) = 0 (Sum.inr k)
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z =
    (B x) x * (B y) z + (2 * (B x) z * (B x) y - 2 * (B x) z * ((B x) x * (coroot B hx) y))

Tactic:
apply_self_mul_coroot_apply

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
hSB : B.IsSymm
y z : M
⊢ (B x) x * (B y) z - 2 * (B x) y * (B x) z = (B x) x * (B y) z + (2 * (B x) z * (B x) y - 2 * (B x) z * (2 * (B x) y))