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

Goal state before:
pp: case h
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 : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0

Tactic:
show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) by rfl

Goal state after:
case h
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 : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (b.repr ↑⟨D'.rep, hD'_mem⟩) ⟨D.rep, hD_mem⟩ = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (linearCombination R (polarSym2 ⇑Q ∘ Sym2.map ⇑bm)) (bm.repr x).sym2Mul -
      (linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) =
    Q x

Tactic:
rw [← apply_linearCombination', Basis.linearCombination_repr]

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

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x✝ : M
x : ι × ι
hx : x ∈ (bm.repr x✝).support.offDiag
⊢ ¬x.1 = x.2

Tactic:
rw [Finset.mem_offDiag] at hx

Goal state after:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x✝ : M
x : ι × ι
hx : x.1 ∈ (bm.repr x✝).support ∧ x.2 ∈ (bm.repr x✝).support ∧ x.1 ≠ x.2
⊢ ¬x.1 = x.2
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (ρ_ X).hom =
    (((Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (𝟙_ (QuadraticModuleCat R)))).symm ≪≫
          (Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X) ⊗ᵢ (Iso.refl (𝟙_ (ModuleCat R))).symm)) ≪≫
        ρ_ ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X)).hom

Tactic:
by
        simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom,
          Iso.refl_hom, MonoidalCategory.tensorIso_hom, MonoidalCategory.id_tensorHom]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        erw [MonoidalCategory.whiskerLeft_id]
        simp
        rfl

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

Goal state before:
pp: case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing 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✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ↥b.support
⊢ (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)

Tactic:
simp [ω, e, f]

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 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
hki : P.root k ≠ P.root i
contra : P.root k = -P.root i
h₁ : P.root l = 0
⊢ False

Tactic:
exact P.ne_zero _ h₁

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

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing 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✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ι
l : ↥b.support
⊢ (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)

Tactic:
simp [ω, e, f]

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 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
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
contra : P.root l = P.root i
h₁ : P.root k = 0
⊢ False

Tactic:
exact P.ne_zero _ h₁

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ IsLieAbelian ↥(cartanSubalgebra' b)

Tactic:
refine ⟨fun ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ ↦ ?_⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ x✝ : ↥(cartanSubalgebra' b)
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
hx' : ⟨x, hx⟩ ∈ cartanSubalgebra' b
y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hy : y ∈ lieAlgebra b
hy' : ⟨y, hy⟩ ∈ cartanSubalgebra' b
⊢ ⁅⟨⟨x, hx⟩, hx'⟩, ⟨⟨y, hy⟩, hy'⟩⁆ = 0
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}
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
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
contra : P.root n = P.root i
⊢ False

Tactic:
by
    replace h₃ : P.root k = P.root j := by
      rwa [contra, add_comm, add_sub_assoc, left_eq_add, sub_eq_zero] at h₃
    replace h₂ : P.root m = 0 := by rw [← h₂, h₃, sub_self]
    exact P.ne_zero _ h₂

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

Goal state before:
pp: case lie
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing 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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x u v : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx✝ : u ∈ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)
hy✝ : v ∈ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)
hu : (ωConj b) u ∈ lieAlgebra b
hv : (ωConj b) v ∈ lieAlgebra b
⊢ ⁅(ωConj b) u, (ωConj b) v⁆ ∈ lieAlgebra b

Tactic:
exact (lieAlgebra b).lie_mem hu hv

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 : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
this :
  ((∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) -
      ∑ x,
        if P.root k = P.root x - P.root ↑i then (↑(chainTopCoeff (↑i) x) + 1) * (↑(chainBotCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)

Tactic:
have aux (x : ι) : P.root x = P.root k - P.root i ↔ P.root k = P.root i + P.root x := by
      rw [eq_sub_iff_add_eq', eq_comm]

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 : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
this :
  ((∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) -
      ∑ x,
        if P.root k = P.root x - P.root ↑i then (↑(chainTopCoeff (↑i) x) + 1) * (↑(chainBotCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)
aux : ∀ (x : ι), P.root x = P.root k - P.root ↑i ↔ P.root k = P.root ↑i + P.root x
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * 2 • (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
smul_eq_mul

Goal state after:
case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * 3 • (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P) =
    3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
smul_eq_mul

Goal state after:
case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (3 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P) =
    3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)
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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l x : ι
⊢ P.root x = P.root l - P.root ↑i → k = i → ¬x = -↑i

Tactic:
rintro contra rfl rfl

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 ι
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
contra : P.root (-↑k) = P.root l - P.root ↑k
⊢ False
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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
h₁ : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ k = i ∧ x = -↑i)
x : ι
⊢ P.root x = P.root ↑i + P.root l → k = i → ¬x = ↑i

Tactic:
rintro contra rfl rfl

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 ι
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
h₁ : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑k ∧ k = k ∧ x = -↑k)
contra : P.root ↑k = P.root ↑k + P.root l
⊢ False
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 k : ↥b.support
l : ι
this : InvolutiveNeg ι := P.indexNeg
aux₁ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ k = j ∧ x = ↑j)
aux₂ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root l - P.root ↑j ∧ k = i ∧ x = -↑i)
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0

Tactic:
simp [e, f, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux₁, Finset.sum_ite_of_false aux₂]

Goal state after:
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
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
z : M
⊢ 2 * (B ↑x) z = 2 * (B ↑y) z

Tactic:
h2x z,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
z : M
⊢ (B ↑x) ↑x * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
ht : t ∈ closedCompactCylinders X
⊢ t = cylinder (closedCompactCylinders.finset ht) (closedCompactCylinders.set ht)

Tactic:
· exact closedCompactCylinders.eq_cylinder ht

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
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1

Tactic:
have : ∃ v, LinearIndependent K ![v, e.fixedReduce v] := by
    contrapose! he
    obtain ⟨a, ha⟩ :=
      LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent h.ne' he
    refine ⟨a, fun x ↦ by
      simp only [← coe_toLinearMap, ha, LinearMap.smul_apply, one_apply, Subring.smul_def]⟩

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
this : ∃ v, LinearIndependent K ![v, e.fixedReduce v]
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ u ⊆ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Tactic:
exact subset_sUnion_of_mem hu

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h : ¬Disjoint I (hC.disjointOfDiffUnion hs hI)
⊢ False

Tactic:
Finset.not_disjoint_iff

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h : ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion hs hI
⊢ False
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: α : Type u_1
𝒜 : Set (Set α)
⊢ generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜

Tactic:
by
  refine le_antisymm (fun s ms ↦ ?_) (generateFrom_mono self_subset_generateSetAlgebra)
  induction s, ms using generateFrom_induction with
  | hC t ht h =>
    clear h
    induction ht with
    | base u u_mem => exact measurableSet_generateFrom u_mem
    | empty => exact @MeasurableSet.empty _ (generateFrom 𝒜)
    | compl u _ mu => exact mu.compl
    | union u v _ _ mu mv => exact MeasurableSet.union mu mv
  | empty => exact MeasurableSpace.measurableSet_empty _
  | compl t _ ht => exact ht.compl
  | iUnion t _ ht => exact .iUnion ht

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
u_ind : ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t
v_ind : ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ v = ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
| union u v _ _ u_ind v_ind =>

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

Goal state before:
pp: V : Type u_1
Ω : Type u_2
m : MeasurableSpace Ω
G : Ω → SimpleGraph V
⊢ Measurable G ↔ ∀ (u v : V), Measurable fun ω ↦ (G ω).Adj u v

Tactic:
simp [measurable_comap_iff, measurable_pi_iff]

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

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hS : (↑(insert i S)).PairwiseDisjoint s
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) = m (s i) + ∑ x ∈ S, m (s x)

Tactic:
simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) = m (s i) + ∑ x ∈ S, m (s x)