mathlib-initiative/mathlib-tactics huggingface dataset:
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
r : R
b : CliffordAlgebra Q
⊢ r • (contractRight b) d = (algebraMap R (CliffordAlgebra Q)) r * (contractRight b) d

Tactic:
Algebra.smul_def

Goal state after:
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
r : R
b : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) r * (contractRight b) d =
    (algebraMap R (CliffordAlgebra Q)) r * (contractRight b) d
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ LinearMap.det (ibc.endHom (transvection fM vM)) = 1 + (ibc.toDual fM) (ε vM)

Tactic:
det_endHom,

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ (algebraMap S R) (LinearMap.det (transvection fM vM)) = 1 + (ibc.toDual fM) (ε vM)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ pinGroup Q ↔ x ∈ pinGroup Q

Tactic:
refine ⟨?_, star_mem⟩
  intro hx
  convert! star_mem hx
  exact (star_star x).symm

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ spinGroup Q ↔ x ∈ spinGroup Q

Tactic:
refine ⟨?_, star_mem⟩
  intro hx
  convert! star_mem hx
  exact (star_star x).symm

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

Goal state before:
pp: case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
⊢ Injective ⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom)

Tactic:
AddMonoidHom.coe_toZModLinearMap,

Goal state after:
case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
⊢ Injective ⇑g.toAddMonoidHom
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := ⋯
N' : Submodule R N := ⋯
P : ↥L →ₗ[R] ↥M' := ⋯
Q : ↥L →ₗ[R] ↥N' := ⋯
L' : Submodule R (↥M' × ↥N') := ⋯
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ L = map (M'.subtype.prodMap N'.subtype) (comap (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ) (↑e).graph)

Tactic:
rw [← he]

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ L =
    map (M'.subtype.prodMap N'.subtype)
      (comap (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ)
        (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range)
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k

Tactic:
← circulant_col_zero_eq v,

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ circulant v k 0 = w k
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

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

Tactic:
Fin.succAbove_castSucc_of_le _ _ h.le

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

Goal state before:
pp: α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B (a, b) (c, d) = 0

Tactic:
simp only [Prod.mk_inj, Ne, not_and_or] at h

Goal state after:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B (a, b) (c, d) = 0
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_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)

Tactic:
simp only [transpose_apply, isSStronglyConnected_iff, not_and, not_forall, not_exists,
        not_lt, nonpos_iff_eq_zero]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ (∀ (i j : n), 0 ≤ A j i) → ∃ x x_1, ∀ (x_2 : Path x x_1), x_2.length = 0
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ (f fun i ↦ (fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) i) = g fun i ↦ (fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) i

Tactic:
simp_rw [MultilinearMap.map_sum_finset]

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ (∑ r ∈ Fintype.piFinset fun i ↦ Finset.univ, f fun i ↦ Pi.single (r i) (x i (r i))) =
    ∑ r ∈ Fintype.piFinset fun i ↦ Finset.univ, g fun i ↦ Pi.single (r i) (x i (r i))
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case smul_tprod
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r✝ : R
f✝ : (i : ι) → A i
⊢ (mul ((tprod R) 1)) (r✝ • (tprod R) f✝) = r✝ • (tprod R) f✝

Tactic:
| smul_tprod =>

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case smul_tprod
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r✝ : R
f✝ : (i : ι) → A i
⊢ (mul (r✝ • (tprod R) f✝)) ((tprod R) 1) = r✝ • (tprod R) f✝

Tactic:
| smul_tprod =>

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝² : CommRing R
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
j : (i : ι) → γ i
⊢ (⨂ₜ[R] (i : ι), g (j i)) ∈ Submodule.span R (Set.range fun j ↦ ⨂ₜ[R] (i : ι), g (j i))

Tactic:
exact Submodule.subset_span ⟨j, rfl⟩

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

Goal state before:
pp: 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
⊢ ∃ g, g • D = E ∧ g • D' = E'

Tactic:
have : FiniteDimensional K (Submodule.span K (Set.range ![D.rep, D'.rep])) :=
    span_of_finite K (Set.finite_range _)

Goal state after:
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, g • D = E ∧ g • D' = E'
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case inr.inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ x + 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

pp: case inr.inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₂ : y ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

Tactic:
· rwa [add_zero]

Goal state after:
case inr.inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₂ : y ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
hF : ∃ a, a ≠ 0 ∧ a ^ 2 ≠ 1
⊢ commutator PSL(2, F) = ⊤

Tactic:
obtain ⟨a, ha, hasq⟩ := hF
  have : Group.IsPerfect SL(2, F) := ⟨SL2.commutator_eq_top ha hasq⟩
  have : Group.IsPerfect (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) := inferInstance
  exact this.commutator_eq_top

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
a : K
ha : f = a • 1
⊢ ↑m = LinearMap.toMatrix' ↑(Matrix.SpecialLinearGroup.toLin' m)

Tactic:
Matrix.SpecialLinearGroup.toLin'_to_linearMap,

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
a : K
ha : f = a • 1
⊢ ↑m = LinearMap.toMatrix' (Matrix.toLin' ↑m)
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
h : Q.Equivalent Q'
⊢ Module.finrank R ↥Q.radical = Module.finrank R ↥Q'.radical

Tactic:
obtain ⟨e⟩ := h

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Module.finrank R ↥Q.radical = Module.finrank R ↥Q'.radical
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
h : Equivalent Q Q'
⊢ sigPos Q = sigPos Q'

Tactic:
obtain ⟨e⟩ := h

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
⊢ sigPos Q = sigPos Q'
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case mem
ι : 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
i : ↥b.support
j : ↥b.support ⊕ ι
x✝ x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
h : x ∈ range GeckConstruction.h
⊢ x j (Sum.inl i) = 0

Tactic:
obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case neg
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2

Tactic:
simp [chainTopCoeff_of_not_linearIndependent, chainBotCoeff_of_not_linearIndependent, h]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
⊢ P.pairingIn ℤ i j ≤ 0

Tactic:
by
  have aux₁ := P.linearIndependent_of_add_mem_range_root' <| add_comm (P.root i) (P.root j) ▸ h
  have aux₂ := P.chainBotCoeff_add_chainTopCoeff_le_two j i
  have aux₃ : 1 ≤ P.chainTopCoeff j i := by
    rwa [← root_add_nsmul_mem_range_iff_le_chainTopCoeff aux₁, one_smul]
  rw [← P.chainBotCoeff_sub_chainTopCoeff aux₁]
  lia

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
χ : ↥H → K
hχ₀ : χ ≠ 0
hχ : genWeightSpace (↥U) χ ≠ ⊥
i : ι
hi : v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
⊢ ∃ i, v b i ∈ U

Tactic:
exact ⟨i, LieSubmodule.map_incl_le hi⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : SymmetricAlgebra R M
⊢ motive a

Tactic:
rcases algHom_surjective _ _ a with ⟨a, rfl⟩
  induction a using TensorAlgebra.induction with
  | algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
  | ι x => exact ι x
  | mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
  | add x y hx hy => rw [map_add]; exact add _ _ hx hy

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (DirectSum.coeAlgHom fun x ↦ (ι R).range ^ x).comp ((lift R) (GradedAlgebra.ι R M)) = AlgHom.id R (TensorAlgebra R M)

Tactic:
by
      ext m
      dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply,
        AlgHom.id_apply]
      rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

Tactic:
refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩

Goal state after:
case inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ s₁.erase a + t + {a} = s₁ + t

case inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
a✝ : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ i_1 ∈ insert i S, s i_1 ∈ C

Tactic:
| insert i S _ h =>

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋃ i ∈ S, s i ∈ C

Tactic:
induction S using Finset.induction with

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C
⊢ ⋂ i, ⋂ (_ : i ≤ n + 1), s i ∈ C

Tactic:
biInter_le_succ

Goal state after:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C
⊢ (⋂ k, ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hSC : ↑S ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
induction S using Finset.induction with

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x) = ⋃₀ ↑J

Tactic:
sUnion_iUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⋃ i ∈ J, ⋃₀ ↑(hC.disjointOfUnion hJ i) = ⋃₀ ↑J
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.top.inl.refine_2
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
hb : ⊤ ∈ Ioi ↑a
ha : Ioi a = ∅
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi ↑x₁)

Tactic:
apply isOpen_generateFrom_of_mem
            simp [d]

Goal state after: