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

Goal state before:
pp: V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : u x = (b.repr (u.rangeRestrict x)) default • ↑(b default)
⊢ (LinearMap.id + u) x = x + (b.coord default ∘ₗ u.rangeRestrict) x • ↑(b default)

Tactic:
by
      simp [this]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
v w : V
⊢ 1 ⊗ₜ[R] (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) v w) =
    1 ⊗ₜ[R] (((QuadraticMap.polarBilin Q) v) w • 1)

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
v w : V
⊢ 1 ⊗ₜ[R] (QuadraticMap.polar (⇑Q) v w • 1) = 1 ⊗ₜ[R] (((QuadraticMap.polarBilin Q) v) w • 1)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : CliffordAlgebra Q
r : R
⊢ (contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) =
    (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂
h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q
⊢ -(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂
h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q
⊢ -((r₁ * r₂) • 1) = r₁ • e0 Q * r₂ • e0 Q
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }
⊢ (fun F ↦ ⟨(F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)), ⋯⟩) ((fun fg ↦ lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg) = fg

Tactic:
ext <;> (dsimp; simp only [map_one, mul_one, one_mul])

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ↥(⋀[R]^i M)
⊢ (liftι R M) ↑x = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i) x

Tactic:
by
  obtain ⟨x, hx⟩ := x
  dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
  induction hx using Submodule.pow_induction_on_left' with
  | algebraMap => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
  | add _ _ _ _ _ ihx ihy => simp_rw [map_add, ihx, ihy, ← map_add]; rfl
  | mem_mul _ hm _ _ _ ih =>
      obtain ⟨_, rfl⟩ := hm
      simp_rw [map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M,
        DirectSum.of_mul_of]
      exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

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

Goal state before:
pp: I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((lof R I A i) 1) = (mkAlgHom R A) 1

Tactic:
exact Quotient.sound <| RingCon.le_ringConGen _ _ <| rel_id R A (i := i)

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

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
r : R
⊢ ((lift R A) fun {i} ↦ maps) ((algebraMap R (FreeProduct R A)) r) = (algebraMap R B) r

Tactic:
rw [lift_apply, AlgHom.commutes]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
σ : Perm n
x✝ : σ ∈ univ
⊢ abv (Perm.sign σ • ∏ i, A (σ i) i) = ∏ i, abv (A (σ i) i)

Tactic:
rw [abv.map_units_int_smul, abv.map_prod]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

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

Tactic:
convert! (Finset.card_image_of_injective Finset.univ f.injective).symm <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

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

Tactic:
neg_eq_iff_add_eq_zero,

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

Goal state before:
pp: m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
⊢ ∀ (x : m × m → k), (eval x) ((p - q) * (Matrix.mvPolynomialX m m k).det) = (eval x) 0

Tactic:
intro s

Goal state after:
m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
s : m × m → k
⊢ (eval s) ((p - q) * (Matrix.mvPolynomialX m m k).det) = (eval s) 0
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case zero.refine_1
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.toQuiver
i j : n
h_pos : 0 < (A ^ 0) i j
⊢ Nonempty { p // p.length = 0 }

Tactic:
rcases eq_or_ne i j with rfl | h_eq
      · exact ⟨⟨Quiver.Path.nil, rfl⟩⟩
      · simp_all

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ ∀ (B : FixedDetMatrix (Fin 2) ℤ m) (n : ℤ), C (T ^ n • B) ↔ C B

Tactic:
intro B n

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
⊢ C (T ^ n • B) ↔ C B
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).IsHadamard

Tactic:
refine ⟨fun _ _ ↦ mul_mem (hA.apply_mem _ _) (hB.apply_mem _ _), ?_, ?_⟩ <;> ext ⟨i, i'⟩ ⟨j, j'⟩

Goal state after:
case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B * (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')

case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ * kroneckerMap (fun x1 x2 ↦ x1 * x2) A B) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 ≠ 0 → (C (reduce (reduceStep A)) → C (reduceStep A)) → C (reduce A) → C A

Tactic:
intro A hc ih hA

Goal state after:
case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
hA : C (reduce A)
⊢ C A
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
⊢ Aᵀ.IsIrreducible

Tactic:
have hA_T_nonneg : ∀ i j, 0 ≤ Aᵀ i j := fun i j => by
    simpa [Matrix.transpose_apply] using hA.nonneg j i
  refine ⟨hA_T_nonneg, ?_⟩
  intro i j
  let : Quiver n := toQuiver A
  obtain ⟨p, hp_pos⟩ := hA.connected j i
  cases p with
  | nil =>
    simp at hp_pos
  | @cons b _ q e =>
    let qT := transposePath (A := A) (q.cons e)
    let : Quiver n := toQuiver Aᵀ
    use qT
    simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
v : ι → M
⊢ (diagonal fun x ↦ r) • v = r • v

Tactic:
ext i
  simp [Matrix.diagonal_apply]

Goal state after:
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)
inst✝ : DecidableEq ι
i : ι
r : R
⊢ tprodCoeff R 1 ((MonoidHom.mulSingle A i) ((algebraMap R (A i)) r)) = r • tprodCoeff R 1 1

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
ι : 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)
inst✝ : DecidableEq ι
i : ι
r : R
⊢ tprodCoeff R 1 ((MonoidHom.mulSingle A i) (r • 1)) = r • tprodCoeff R 1 1
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])) :=
  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)))

Tactic:
simp [f]

Goal state after:
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])) :=
  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 1 1)) = ↑(f (hD.linearCombinationEquiv (Finsupp.single 1 1)))

Tactic:
simp [f]

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

Goal state before:
pp: 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
this : ∀ (a : Kˣ), ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
⊢ ∃ g, g • D = E ∧ g • D' = E'

Tactic:
obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹

Goal state after:
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
this : ∀ (a : Kˣ), ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
h : V ≃ₗ[K] V
hdet : LinearEquiv.det h = (LinearEquiv.det g)⁻¹
hD : h • D = D
hE : h • D' = D'
⊢ ∃ g, g • D = E ∧ g • D' = E'
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
⊢ iSup iwasawaT = ⊤

Tactic:
have step1 : iSup (PSL.iwasawaT (F := F) (ι := Fin 2)) =
      Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)))
        (⨆ p : ℙ F (Fin 2 → F),
          Matrix.SpecialLinearGroup.lineStab (F := F) (ι := Fin 2) p.submodule) := by
    rw [Subgroup.map_iSup]

Goal state after:
F : Type u_2
inst✝ : Field F
step1 : iSup iwasawaT = Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (⨆ p, lineStab p.submodule)
⊢ iSup iwasawaT = ⊤
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

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

Tactic:
refine Subtype.ext <| ext_iff_smul.2 fun w ↦ ?_
  obtain ⟨α, hα⟩ := Submodule.mem_span_singleton.mp (hA w)
  obtain ⟨β, hβ⟩ := Submodule.mem_span_singleton.mp (hB w)
  simp only [coe_mul, mul_smul, ← Matrix.SpecialLinearGroup.smul_def]
  rw [← sub_add_cancel (A • w) w, ← hα, ← sub_add_cancel (B • w) w,
    ← hβ, smul_add, smul_add, ← sub_left_inj (a := w), ← add_sub, ← hα, ← add_sub, ← hβ,
    smul_comm, lineStab_fix_of_span v hv A hA, smul_comm, lineStab_fix_of_span v hv B hB, add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (((Iso.refl (ModuleCat.of R ↑(X ⊗ Y).toModuleCat ⊗ ModuleCat.of R ↑Z.toModuleCat)).symm ≪≫
          ((Iso.refl (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑Y.toModuleCat)).symm ⊗ᵢ
            Iso.refl (ModuleCat.of R ↑Z.toModuleCat))) ≪≫
        α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑Y.toModuleCat) (ModuleCat.of R ↑Z.toModuleCat) ≪≫
          (Iso.refl (ModuleCat.of R ↑X.toModuleCat) ⊗ᵢ
              Iso.refl (ModuleCat.of R ↑Y.toModuleCat ⊗ ModuleCat.of R ↑Z.toModuleCat)) ≪≫
            Iso.refl (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑(Y ⊗ Z).toModuleCat)).hom

Tactic:
simp only [Iso.refl_symm, Iso.trans_hom,
          MonoidalCategory.tensorIso_hom, Iso.refl_hom, MonoidalCategory.id_tensorHom_id]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 (ModuleCat.of R ↑(X ⊗ Y).toModuleCat ⊗ ModuleCat.of R ↑Z.toModuleCat) ≫
        (𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑Y.toModuleCat) ⊗ₘ 𝟙 (ModuleCat.of R ↑Z.toModuleCat))) ≫
      (α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑Y.toModuleCat) (ModuleCat.of R ↑Z.toModuleCat)).hom ≫
        𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑Y.toModuleCat ⊗ ModuleCat.of R ↑Z.toModuleCat) ≫
          𝟙 (ModuleCat.of R ↑X.toModuleCat ⊗ ModuleCat.of R ↑(Y ⊗ Z).toModuleCat)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
⊢ x = 0

Tactic:
by_contra hx'

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
hx' : ¬x = 0
⊢ 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
⊢ False

Tactic:
replace h₃ : P.root n = 2 • P.root i := by rw [h₃, h₂]; abel

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 : ι
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
h₃ : P.root n = 2 • P.root i
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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✝⁹ : 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 ι
i j : ι
k : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
l : ↥b.support
h : i ≠ -↑k
⊢ ⁅e k, v b i⁆ (Sum.inl l) = ((↑(chainBotCoeff (↑k) i) + 1) • v b j) (Sum.inl l)

Tactic:
simp [e, h, -indexNeg_neg]

Goal state after: