mathlib-initiative/mathlib-tactics huggingface dataset:
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 ^ max (Module.finrank R V) 1 = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)

Tactic:
have : IsUnit r := by
          rw [← isUnit_pow_iff _, hr]
          · exact isUnit_one
          rw [Nat.max_eq_left hV]
          exact Nat.ne_zero_of_lt 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
this : IsUnit r
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
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))
⊢ centerEquivRootsOfUnity_invFun
      ((fun g ↦
          ⋯.by_cases (fun x ↦ 1) fun hR ↦
            ⋯.by_cases (fun x ↦ 1) fun hV ↦
              have hV := ⋯;
              have hr := ⋯;
              let r := ⋯.choose;
              have this := ⋯;
              ⟨this.unit, ⋯⟩)
        g) =
    g

Tactic:
simp only [centerEquivRootsOfUnity_invFun, ← Subtype.val_inj,
      ← LinearEquiv.toLinearMap_inj, LinearMap.coe_equivOfIsUnitDet]

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))
⊢ ↑↑(⋯.by_cases (fun x ↦ 1) fun hR ↦ ⋯.by_cases (fun x ↦ 1) fun hV ↦ ⟨⋯.unit, ⋯⟩) • LinearMap.id = ↑↑↑g
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 h : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ (⋯.by_cases (fun x ↦ 1) fun hR ↦
      ⋯.by_cases (fun x ↦ 1) fun hV ↦
        have hV := ⋯;
        have hr := ⋯;
        let r := ⋯.choose;
        have this := ⋯;
        ⟨this.unit, ⋯⟩) =
    (⋯.by_cases (fun x ↦ 1) fun hR ↦
        ⋯.by_cases (fun x ↦ 1) fun hV ↦
          have hV := ⋯;
          have hr := ⋯;
          let r := ⋯.choose;
          have this := ⋯;
          ⟨this.unit, ⋯⟩) *
      ⋯.by_cases (fun x ↦ 1) fun hR ↦
        ⋯.by_cases (fun x ↦ 1) fun hV ↦
          have hV := ⋯;
          have hr := ⋯;
          let r := ⋯.choose;
          have this := ⋯;
          ⟨this.unit, ⋯⟩

Tactic:
by
    simp only [Or.by_cases, Subgroup.coe_mul, coe_mul, LinearEquiv.coe_toLinearMap_mul,
      mul_dite, mul_one, dite_mul, one_mul, MulMemClass.mk_mul_mk]
    split_ifs with hR hV
    · rfl
    · rfl
    rw [not_subsingleton_iff_nontrivial] at hV
    have := Module.Free.instFaithfulSMulOfNontrivial R V
    set Hg := (mem_center_iff.mp g.prop)
    set Hh := (mem_center_iff.mp h.prop)
    set Hgh := (mem_center_iff.mp (g * h).prop)
    simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec, Units.val_mul]
    change Hgh.choose = Hg.choose * Hh.choose
    suffices (Hgh.choose • LinearMap.id : V →ₗ[R] V)
      = (Hg.choose • LinearMap.id) * (Hh.choose • LinearMap.id) by
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp [mul_smul,
        ← mem_center_iff_spec (g * h).prop, ← mem_center_iff_spec h.prop,
        ← mem_center_iff_spec g.prop]
    simp [← Hgh.choose_spec.2, ← Hh.choose_spec.2, ← Hg.choose_spec.2]

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

Goal state before:
pp: case inl
ι : 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
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : 0 < P.pairingIn ℤ j k
⊢ P.root k - P.root j ∈ range ⇑P.root

pp: case inr
ι : 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
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
⊢ P.root k - P.root j ∈ range ⇑P.root

Tactic:
· rw [← neg_mem_range_root_iff, neg_sub]
    exact P.root_sub_root_mem_of_pairingIn_pos hm hkj.symm

Goal state after:
case inr
ι : 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
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
⊢ P.root k - P.root j ∈ range ⇑P.root
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 : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
hk : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
⊢ -k ≠ i

Tactic:
contrapose hkj

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
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
hk : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hkj : -k = i
⊢ P.root k = -P.root i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inl
ι : 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
k : ι
⊢ ∑ x ∈ {k, k},
      ((if P.root x = P.root ↑i + P.root k then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) k) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x k
        else 0) =
    if P.root k = P.root ↑i + P.root k then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) k) + ↑(b.cartanMatrix i j)
    else 0

Tactic:
simp [P.ne_zero i]

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

Goal state before:
pp: case h.inl
ι : 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 ι
i : ↥b.support
this✝² : Module.IsReflexive R M
this✝¹ : IsAddTorsionFree M
this✝ : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
this : (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0
⊢ (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0

Tactic:
assumption

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

Goal state before:
pp: case inl
ι : 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ↥b.support
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)

Tactic:
have : χ x ≠ 0 := hχx ▸ hd₀ i

Goal state after:
case inl
ι : 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ↥b.support
this : χ x ≠ 0
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ (B (b.equivFun.symm x)) (b.equivFun.symm x)

Tactic:
exact h _

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ star ⇑(b.repr x) ⬝ᵥ ((toMatrix₂ b b) B).mulVec ⇑(b.repr x)

Tactic:
exact h _

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
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
this : v b ↑j ∈ ↑U
⊢ v b ↑j ∈ U

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case symm
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ : ⨂[R] (x : ι), M
a✝ : AddConGen.Rel (Rel R ι M) x✝ y✝
a_ih✝ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) (r • y✝)

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) ?trans.y

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case trans.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • y✝) (r • z✝)

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case add.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • w✝) (r • x✝)

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • y✝) (r • z✝)

Tactic:
assumption

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

Goal state before:
pp: case right
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
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
ht : (↑e).fixedSubmodule ≤ (↑(transvection hfv)).fixedSubmodule
⊢ v ∈ (↑(transvection hfv * e)).fixedSubmodule

Tactic:
· -- u ∈ e.fixedSubmodule
    simp only [mem_fixedSubmodule_iff, LinearEquiv.coe_toLinearMap,
      LinearEquiv.mul_apply, transvection.apply]
    simp [hfv']

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 f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ f (u - e u) = 0

Tactic:
simp only [← LinearMap.mem_ker]

Goal state after:
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
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ u - e u ∈ ker f
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hv
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' : f u = 0
⊢ False

Tactic:
simp [hu'] at hfu

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
W : Submodule K V
v : V
hW : 1 < finrank K (V ⧸ W)
htop : W ⊔ K ∙ v = ⊤
h1 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K ↥(W ⊔ K ∙ v) ≤ finrank K ↥W + 1

Tactic:
refine le_trans (Submodule.finrank_add_le_finrank_add_finrank _ _) ?_

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hW : 1 < finrank K (V ⧸ W)
htop : W ⊔ K ∙ v = ⊤
h1 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K ↥W + finrank K ↥(K ∙ v) ≤ finrank K ↥W + 1
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
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
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
⊢ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f

Tactic:
simpa [hf] using hf (sub_mem_comm_iff.mp hv')

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
⊢ (auxTransvection ⋯ * e) w - w ∈ (↑e).fixedSubmodule ⊔ K ∙ v

Tactic:
simp only [auxTransvection, LinearEquiv.mul_apply, transvection.apply,
          add_sub_right_comm]

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 := 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
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S

Tactic:
refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
⊢ MeasurableSet ((fun j ↦ if hji : j = i then ⋯.mpr t else univ) j)

case refine_2
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ eval i ⁻¹' (fun j ↦ if hji : j = i then ⋯.mpr t else univ) i = S
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ cylinder s univ = univ

Tactic:
by
  rw [cylinder, preimage_univ]

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

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

Tactic:
rw [mem_measurableCylinders] at *
  obtain ⟨s₁, S₁, hS₁, rfl⟩ := hs
  obtain ⟨s₂, S₂, hS₂, rfl⟩ := ht
  classical
  refine ⟨s₁ ∪ s₂,
    Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
      {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_, ?_⟩
  · refine MeasurableSet.inter ?_ ?_
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₂
  · exact inter_cylinder _ _ _ _

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

Goal state before:
pp: case convert_2.«0».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ (if h : ∃ p, p.1 ≤ p.2 ∧ ∅ = Set.Ioc p.1 p.2 then f h.choose.2 - f h.choose.1 else 0) = 0

Tactic:
dite_eq_right_iff

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ ∀ (h : ∃ p, p.1 ≤ p.2 ∧ ∅ = Set.Ioc p.1 p.2), f h.choose.2 - f h.choose.1 = 0
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
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
x : V
hx : x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v)
⊢ f x + g x = 0

Tactic:
mem_ker.mp (hf hx),

Goal state after:
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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
x : V
hx : x ∈ (↑e).fixedSubmodule ⊔ K ∙ (e v - v)
⊢ 0 + g x = 0