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

Goal state before:
pp: α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0 D).IsDiag

Tactic:
by
  rintro (i | i) (j | j) hij
  · exact ha (ne_of_apply_ne _ hij)
  · rfl
  · rfl
  · exact hd (ne_of_apply_ne _ hij)

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), IsIdempotentElem (f.ofConv i j)
⊢ IsSelfAdjoint f

Tactic:
IsIdempotentElem.iff_eq_zero_or_one

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
⊢ IsSelfAdjoint f
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✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
⊢ ∀ (x y : R'), (x + y) • 1 = x • 1 + y • 1

Tactic:
simp [add_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : Independent ![mk K v hv, mk K w hw]
⊢ IsCollinear {mk K v hv, mk K w hw}

Tactic:
independent_mk_iff_LinearIndependent

Goal state after:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ IsCollinear {mk K v hv, mk K w hw}
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ Module.finrank K ↥(Submodule.span K (Set.range ![v, w])) ≤ 2

Tactic:
simp [finrank_span_eq_card h]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
v : V
hv : v ≠ 0
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
w : V
hw : w ≠ 0
hp3 : mk K w hw ∈ Submodule.projectivization p
hq3 : mk K w hw ∈ Submodule.projectivization q
hxy : Independent ![mk K v hv, mk K w hw]
⊢ p = q

Tactic:
independent_mk_iff_LinearIndependent

Goal state after:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
v : V
hv : v ≠ 0
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
w : V
hw : w ≠ 0
hp3 : mk K w hw ∈ Submodule.projectivization p
hq3 : mk K w hw ∈ Submodule.projectivization q
hxy : LinearIndependent K ![v, w]
⊢ p = q
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
⊢ ∃ g, g • D = E ∧ g • D' = E'

pp: case neg
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ ∃ g, g • D = E ∧ g • D' = E'

Tactic:
· suffices ∀ a : Kˣ, ∃ h : V ≃ₗ[K] V, h.det = a ∧ h • D = D ∧ h • D' = D' by
      obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹
      use ⟨g * h, by simp [hdet]⟩
      simp [specialLinearGroup_smul_def, toLinearEquiv_eq_coe, mul_smul, gD, hD, gE, hE]
    intro a
    rw [← linearIndependent_pair_iff_ne] at hD
    have := linearIndepOn_pair D D'
    let s := (linearIndepOn_pair D D').extend (Set.subset_univ _)
    let b : Module.Basis s K V := Module.Basis.extend this
    rw [← mk_rep D, ← mk_rep D']
    have hD_mem : D.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)
    have hD'_mem : D'.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)
    refine ⟨dilatransvection (f := b.coord ⟨D.rep, hD_mem⟩)
      (v := (a.val - 1) • b ⟨D.rep, hD_mem⟩) (by simp), ?_, ?_, ?_⟩
    · simp [← Units.val_inj, coe_det, LinearMap.transvection.det]
    · rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]
      use a
      rw [← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]
      suffices (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1 by
        rw [this, Module.Basis.extend_apply_self, Units.smul_def]
        module
      nth_rewrite 1 [show D.rep = (⟨D.rep, hD_mem⟩ : s) by rfl]
      rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
      simp
    · rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]
      use 1
      rw [one_smul, ← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]
      suffices (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0 by
        rw [Module.Basis.extend_apply_self]
        simp [this]
      nth_rewrite 1 [show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) by rfl]
      rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
      apply Finsupp.single_eq_of_ne
      simp only [ne_eq, ← Subtype.coe_inj]
      intro h
      apply Fin.zero_ne_one
      apply hD.injective
      simp [h]

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ ∃ g, g • D = E ∧ g • D' = E'
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inr
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
simp_rw [h, pow_one] at this

Goal state after:
case inr
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
this : ↑↑r = 1
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) := (centerCongr (toLin_equiv b)) g
hgg' : ∀ (x : V), ↑↑↑g' x = ↑↑((toLin_equiv b) ↑g) x
x : V
⊢ (↑↑(centerEquivRootsOfUnity g') • LinearMap.id) x = (↑↑(center_equiv_rootsOfUnity g) • LinearMap.id) x

Tactic:
have := centerEquivRootsOfUnity_apply_apply g' x

Goal state after:
case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this✝ : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) := (centerCongr (toLin_equiv b)) g
hgg' : ∀ (x : V), ↑↑↑g' x = ↑↑((toLin_equiv b) ↑g) x
x : V
this : centerEquivRootsOfUnity g' • x = (fun x ↦ ↑↑g' x) x
⊢ (↑↑(centerEquivRootsOfUnity g') • LinearMap.id) x = (↑↑(center_equiv_rootsOfUnity g) • LinearMap.id) x
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: 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

Tactic:
by
  constructor
  · exact fun hN ↦ ⟨Q.lift N hN, rfl⟩
  · rintro ⟨Q', rfl⟩ m hm
    simp [radical, (Submodule.Quotient.mk_eq_zero _).mpr hm, LinearMap.ext_iff, polar]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃

Tactic:
by
  refine (QuadraticMap.associated_rightInverse R).injective ?_
  ext m₁ m₂ m₁' m₂' m₁'' m₂''
  simp only [associated_tmul, QuadraticMap.associated_comp]
  exact mul_assoc _ _ _

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

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

Tactic:
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]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0) ↔
    ∀ i ∉ {i | w i = 0}, v i = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
i : ↥b.support
⊢ (trace R (↥b.support ⊕ ι → R)) ((toEnd R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R)) (f i)) = 0

Tactic:
· simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_f i)

Goal state after:
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
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
⊢ P.root n - P.root k = P.root i - P.root j

Tactic:
hn

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
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
⊢ P.root k + P.root i - P.root j - P.root k = P.root i - P.root j
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : genWeightSpace (↥U) 0 = ⊤
⊢ U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)

Tactic:
by simp [this]

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ i, v b i ∈ U

Tactic:
by
  suffices ∃ χ : H → K, χ ≠ 0 ∧ genWeightSpace U χ ≠ ⊥ by
    obtain ⟨χ, hχ₀, hχ⟩ := this
    obtain ⟨i, hi⟩ := instIsIrreducible_aux₀ χ hχ₀ hχ
    exact ⟨i, LieSubmodule.map_incl_le hi⟩
  contrapose! hU
  refine le_trans ?_ (map_genWeightSpace_le (f := U.incl))
  suffices genWeightSpace U (0 : H → K) = ⊤ by simp [this]
  have : ⨆ (χ : H → K), ⨆ (_ : χ ≠ 0), (⊥ : LieSubmodule K H U) = ⊥ := biSup_const ⟨1, one_ne_zero⟩
  rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]

Goal state after:
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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
aux₃ : ∀ (x : ι), x ≠ m → ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
aux₄ : ∀ (x : ι), x ≠ l' → ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ P.root l' = P.root ↑i + P.root l

Tactic:
hl',

Goal state after:
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
aux₃ : ∀ (x : ι), x ≠ m → ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
aux₄ : ∀ (x : ι), x ≠ l' → ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ P.root l + P.root ↑i = P.root ↑i + P.root l
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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
aux₃ : ∀ (x : ι), x ≠ m → ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
aux₄ : ∀ (x : ι), x ≠ l' → ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ P.root k = P.root l' - P.root ↑j

Tactic:
hl',

Goal state after:
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
aux₃ : ∀ (x : ι), x ≠ m → ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
aux₄ : ∀ (x : ι), x ≠ l' → ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ P.root k = P.root l + P.root ↑i - P.root ↑j
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
this : finrank K ↥((↑e).fixedSubmodule ⊓ (↑f).fixedSubmodule) ≤ finrank K ↥(↑e ∘ₗ ↑f).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
rwa [← Nat.add_le_add_iff_left, finrank_sup_add_finrank_inf_eq] at this

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

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu : u ∉ (↑e).fixedSubmodule
⊢ finrank K (V ⧸ (↑(auxTransvection hf * e)).fixedSubmodule) + 1 = finrank K (V ⧸ (↑e).fixedSubmodule)

Tactic:
rw [auxTransvection_mul_fixed hfu]
  exact finrank_quotient_sup_span_singleton hu

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_1.refine_2
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
⊢ t₂' i ∈ C i

Tactic:
by_cases hi₂ : i ∈ s₂
      · rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)
      · rw [h2' i hi₂]
        exact hC_univ i

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

Goal state before:
pp: case refine_2.he
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := auxTransvection ⋯
ht : t = auxTransvection ⋯
he : ∀ (v : V), e v - v ∈ (↑e).fixedSubmodule
w : V
⊢ e w - w + f (e w) • (v - e v) ∈ (↑e).fixedSubmodule ⊔ K ∙ v

Tactic:
apply mem_sup_left

Goal state after:
case refine_2.he
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
t : V ≃ₗ[K] V := ⋯
ht : t = auxTransvection ⋯
he : ∀ (v : V), e v - v ∈ (↑e).fixedSubmodule
w : V
⊢ e w - w + f (e w) • (v - e v) ∈ (↑e).fixedSubmodule
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ MeasurableSet s

Tactic:
by
  obtain ⟨I, t, mt, rfl⟩ := (mem_measurableCylinders s).1 hs
  exact mt.cylinder

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion hs hI, m u = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

Tactic:
sum_union

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ x ∈ I, m x + ∑ x ∈ hC.disjointOfDiffUnion hs hI, m x = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ Disjoint I (hC.disjointOfDiffUnion hs hI)