mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
this : μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0
⊢ ∫ (x : α) in t, μ[s.indicator f | m] x ∂μ.restrict sᶜ = 0

Tactic:
calc
        ∫ x : α in t, (μ[s.indicator f | m]) x ∂μ.restrict sᶜ =
            ∫ x : α in t, 0 ∂μ.restrict sᶜ := by
          refine setIntegral_congr_ae (hm₂ _ ht) ?_
          filter_upwards [this] with x hx _ using hx
        _ = 0 := integral_zero _ _

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]

Tactic:
apply condExp_congr_ae

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ (fun x ↦ (ENNReal.ofReal (f x)).toReal) =ᵐ[μ] f
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:

Tactic:
∫ x in g ⁻¹' t, ((μ.map g).rnDeriv (ν.map g) (g x)).toReal ∂ν
    _ = ∫ y in t, ((μ.map g).rnDeriv (ν.map g) y).toReal ∂(ν.map g) := by
      rw [setIntegral_map ht _ hg.aemeasurable]
      exact Measurable.aestronglyMeasurable (by fun_prop)
    _ = ∫ x in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν := by
      rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (ω : Ω) in s, c * P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P

Tactic:
lintegral_const_mul' _ _ hc,

Goal state after:
case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ c * ∫⁻ (a : Ω) in s, P⁻[X | mΩ] a ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ c * ∫⁻ (a : Ω) in s, P⁻[X | mΩ] a ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P

Tactic:
lintegral_const_mul' _ _ hc,

Goal state after:
case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ c * ∫⁻ (a : Ω) in s, P⁻[X | mΩ] a ∂P = c * ∫⁻ (a : Ω) in s, X a ∂P
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
⊢ ∑ l, (A * b.toMatrix p) i l = 1

Tactic:
by simp [hA, Matrix.one_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), w j ∈ Set.Icc 0 1
j : Fin n
hji : j ≠ i
⊢ 0 ≤ x⁻¹ * w j

Tactic:
exact mul_nonneg (by simpa using hxpos.le) (hj j).1

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
σ : Perm (ιa ⊕ ιb)
⊢ ∑ y with ⟦y⟧ = Quotient.mk'' σ, sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Tactic:
| h σ =>

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

Goal state before:
pp: case mp
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
⊢ (∃ f v, ↑e = LinearMap.transvection f v) → Module.rank K ↥(↑e - LinearMap.id).range ≤ 1

Tactic:
rintro ⟨f, v, he⟩

Goal state after:
case mp
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : ↑e = LinearMap.transvection f v
⊢ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
cases (isEmpty_or_nonempty n).symm

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ (M ^ Fintype.card K).charpoly = M.charpoly
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case succ
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
⊢ (M.submatrix i.succ.succAbove id).det = (↑↑i + 1).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
Int.negOnePow_succ,

Goal state after:
case succ
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
⊢ (M.submatrix i.succ.succAbove id).det = -(↑↑i).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
x✝ :
  Monotone l ∧
    StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
hmono : Monotone l
hstrict : StrictMonoOn l {i | l i ≠ ⊤}
hlead : ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
i₁ i₂ : m
hlt : i₁ < i₂
j₂ : n
hz : ∀ j₁ < j₂, A i₁ j₁ = 0
h₂ : l i₂ = ⊤
⊢ ↑j₂ < l i₂

Tactic:
h₂

Goal state after:
case inl
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
x✝ :
  Monotone l ∧
    StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
hmono : Monotone l
hstrict : StrictMonoOn l {i | l i ≠ ⊤}
hlead : ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
i₁ i₂ : m
hlt : i₁ < i₂
j₂ : n
hz : ∀ j₁ < j₂, A i₁ j₁ = 0
h₂ : l i₂ = ⊤
⊢ ↑j₂ < ⊤
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
i : m
⊢ ((∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) ↔
    l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c

Tactic:
cases l i <;> simp [IsLeadingEntry, funext_iff]

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

Goal state before:
pp: case mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
⊢ A.IsIrreducible → ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

pp: case mpr
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
⊢ (∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j) → A.IsIrreducible

Tactic:
· intro h_irr i j
    obtain ⟨p, hp_len⟩ := h_irr.2 i j
    refine ⟨p.length, hp_len, ?_⟩
    have : Nonempty {q : Path i j // q.length = p.length} := ⟨⟨p, rfl⟩⟩
    have hpos :=
      (pow_apply_pos_iff_nonempty_path (A := A) hA p.length i j).2 this
    simpa using hpos

Goal state after:
case mpr
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
⊢ (∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j) → A.IsIrreducible
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‖
⊢ ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A.transpose k j‖ < ‖A.transpose k k‖

Tactic:
by simp_rw [Matrix.transpose_apply]; exact h

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

Goal state before:
pp: case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ diagonal A.diag i i = A i i

Tactic:
diagonal_apply_eq,

Goal state after:
case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ A.diag i = A i i
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ 0 = A i j

Tactic:
h hij

Goal state after:
case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ 0 = 0
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.Nonsingular

Tactic:
by
  intro a b bal
  let P (r : ℕ) : Prop := ∀ f g : Fin r → n, (A.submatrix f g).IsDetpBalanced a b
  suffices h : P 0 by simpa [IsDetpBalanced] using h Fin.elim0 Fin.elim0
  refine Nat.decreasingInduction' (n := Fintype.card n) (fun r _ _ ih f g ↦ ?_) (Nat.zero_le _) <|
    bal.submatrix_of_card_le (Fintype.card_fin _).ge
  by_cases hg : g.Surjective
  · exact bal.submatrix_of_card_le (Fintype.card_le_of_surjective g hg) f g
  obtain ⟨j₀, h₀⟩ := by simpa [Function.Surjective] using hg
  let D := A.submatrix f g
  let Aj (j : Fin r) := A.submatrix f (Function.update g j j₀)
  let v (a b : R) : n →₀ R := ∑ j, .single (g j) (a * (Aj j).detp (-1) + b * (Aj j).detp 1) +
    .single j₀ (a * D.detp 1 + b * D.detp (-1))
  suffices h : v a b = v b a by simpa [IsDetpBalanced, v, h₀] using congr($h j₀)
  refine ind (funext fun i ↦ ?_)
  let Ai := A.submatrix (Option.rec i f) (Option.rec j₀ g)
  have (s : ℤˣ) : Ai.detp s = ∑ j, (Aj j).detp (-s) * A.col (g j) i + D.detp s * A.col j₀ i := by
    simp_rw [mul_comm]; rw [detp_option_expand_row_none, add_comm]
    congr!; aesop (add simp Function.update)
  have (a b : R) : (v a b).linearCombination R A.col i = a * Ai.detp 1 + b * Ai.detp (-1) := by
    simp [v, Finset.sum_add_distrib, mul_assoc, ← Finset.mul_sum, add_add_add_comm, mul_add, this]
  simpa [this, IsDetpBalanced, ← submatrix_submatrix] using
    ih (Option.rec i f ∘ finSuccEquiv r) (Option.rec j₀ g ∘ finSuccEquiv r)

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ (equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), m i) = ((tprod R) fun j ↦ m ↑j) ⊗ₜ[R] m i₀

Tactic:
dsimp [equivPiTensorComplSingletonTensor]

Goal state after:
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ (LinearEquiv.lTensor (⨂[R] (i₁ : { i // ¬i = i₀ }), M ↑i₁) (subsingletonEquiv ()))
      ((tmulEquivDep R fun i ↦
            M ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm i))).symm
        ((reindex R M ((Equiv.optionSubtypeNe i₀).symm.trans (Equiv.optionEquivSumPUnit { i // ¬i = i₀ })))
          (⨂ₜ[R] (i : ι), m i))) =
    ((tprod R) fun j ↦ m ↑j) ⊗ₜ[R] m i₀
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) := ⋯
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ 1 • E.rep = g • D.rep

Tactic:
simp only [one_smul, LinearEquiv.smul_def, ← qD hD, ← hg, ← qD hE]

Goal state after:
case h
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ ↑(hE.linearCombinationEquiv (Finsupp.single 0 1)) = ↑(f (hD.linearCombinationEquiv (Finsupp.single 0 1)))
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ Module.finrank R V = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)

Tactic:
← Nat.max_eq_left hV

Goal state after:
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case w
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
n : M
hn : n ∈ N
⊢ ∀ (x : M), (Q.polarBilin x) n = 0 x

Tactic:
polarBilin_apply_apply,

Goal state after:
case w
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
n : M
hn : n ∈ N
⊢ ∀ (x : M), polar (⇑Q) x n = 0 x
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w : ι → 𝕜
⊢ (weightedSumSquares 𝕜 w).radical = Pi.spanSubset 𝕜 {i | w i = 0}

Tactic:
by
  classical
  ext v
  simp only [mem_radical_iff', weightedSumSquares_apply, ← pow_two, smul_eq_mul, Pi.add_apply,
    add_sq, mul_add, sum_add_distrib, add_eq_right, Pi.mem_spanSubset_iff]
  constructor
  · rintro ⟨hv, hvv'⟩ i
    simpa [hv, Pi.single_apply, NeZero.ne, or_iff_not_imp_left] using hvv' (Pi.single i 1)
  · simpa only [← sum_add_distrib]
      using fun h ↦ ⟨sum_eq_zero (by grind), fun v ↦ sum_eq_zero (by grind)⟩

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

Goal state before:
pp: case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ∃ x, ¬v x = 0
⊢ ∃ i ∈ univ, 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
obtain ⟨i, hi⟩ := hv'

Goal state after:
case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
i : ι
hi : ¬v i = 0
⊢ ∃ i ∈ univ, 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ i k ≤ -2
hk' : P.root i ≠ -P.root k
⊢ P.pairingIn ℤ k i = -1

Tactic:
have aux (h : P.pairingIn ℤ i k = -2) : ¬P.pairingIn ℤ k i = -2 := by
      have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
      contrapose hk'; exact (P.pairingIn_neg_two_neg_two_iff ℤ i k).mp ⟨h, hk'⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ i k ≤ -2
hk' : P.root i ≠ -P.root k
aux : P.pairingIn ℤ i k = -2 → ¬P.pairingIn ℤ k i = -2
⊢ P.pairingIn ℤ k i = -1
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
⊢ False

Tactic:
let A : ℤ := P.pairingIn ℤ j i

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
h₂ : P.root k = P.root i + P.root j
⊢ P.root k + P.root i - P.root j = 2 • P.root i

Tactic:
h₂

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
h₂ : P.root k = P.root i + P.root j
⊢ P.root i + P.root j + P.root i - P.root j = 2 • P.root i