mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : (weight w) x = m
h✝ : m = n
⊢ coeff x p = coeff x p

pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : (weight w) x = m
h✝ : ¬m = n
⊢ coeff x p = coeff x 0

pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬(weight w) x = m
h✝ : m = n
⊢ 0 = coeff x p

pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬(weight w) x = m
h✝ : ¬m = n
⊢ 0 = coeff x 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : (weight w) x = m
h✝ : m = n
⊢ coeff x p = coeff x p

case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : (weight w) x = m
h✝ : ¬m = n
⊢ coeff x p = coeff x 0

case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬(weight w) x = m
h✝ : m = n
⊢ 0 = coeff x p

case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬(weight w) x = m
h✝ : ¬m = n
⊢ 0 = coeff x 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
⊢ [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥,
      ∀ (m : M), φ m = 0 → m = 0].TFAE

Tactic:
by
  have := (hasEigenvalue_zero_tfae φ).not
  dsimp only [List.map] at this
  push Not at this
  have aux₁ : ∀ m, (m ≠ 0 → φ m ≠ 0) ↔ (φ m = 0 → m = 0) := by intro m; apply not_imp_not
  have aux₂ : ker φ = ⊥ ↔ ¬ ⊥ < ker φ := by rw [bot_lt_iff_ne_bot, not_not]
  simpa only [aux₁, aux₂] using this

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case hg
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Free.chooseBasis R M).end φ i).IsHomogeneous 1

Tactic:
exact LinearMap.toMvPolynomial_isHomogeneous _ _ _

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ F - G = 0

Tactic:
apply eq_zero_of_forall_eval_eq_zero_of_le_card (hF.sub hG) _ hnR

Goal state after:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ ∀ (r : σ → R), (eval r) (F - G) = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case mp
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b).coeff k = 0 → (φ.polyCharpoly b').coeff k = 0

pp: case mpr
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b').coeff k = 0 → (φ.polyCharpoly b).coeff k = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b).coeff k = 0 → (φ.polyCharpoly b').coeff k = 0

case mpr
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b').coeff k = 0 → (φ.polyCharpoly b).coeff k = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b ≤ (φ.polyCharpoly b').natTrailingDegree

pp: case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ (φ.polyCharpoly b').natTrailingDegree ≤ φ.nilRankAux b

Tactic:
<;>

Goal state after:
case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b ≤ (φ.polyCharpoly b').natTrailingDegree

case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ (φ.polyCharpoly b').natTrailingDegree ≤ φ.nilRankAux b
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
h✝ : n = degree d
⊢ (rename φ) ((monomial d) c) = (monomial (mapDomain φ d)) c

pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
h✝ : ¬n = degree d
⊢ (rename φ) 0 = 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
h✝ : n = degree d
⊢ (rename φ) ((monomial d) c) = (monomial (mapDomain φ d)) c

case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
h✝ : ¬n = degree d
⊢ (rename φ) 0 = 0
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: case smul
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
t : R
y : L
hx✝ : y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy : χ y = 0
⊢ χ (t • y) = 0

Tactic:
rw [map_smul, hy, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ derivedSeries R L 1
⊢ χ x = 0

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ←
    LieSubmodule.mem_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span] at h
  induction h using Submodule.span_induction with
  | mem y h =>
    simp only [Subtype.exists, LieSubmodule.mem_top, exists_const, Set.mem_ofPred_eq] at h
    obtain ⟨z, w, rfl⟩ := h
    exact lieCharacter_apply_lie ..
  | zero => exact map_zero _
  | add y z _ _ hy hz => rw [map_add, hy, hz, add_zero]
  | smul t y _ hy => rw [map_smul, hy, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: case mpr
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) ↦ f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s

Tactic:
rintro ⟨s, rfl, si⟩
    exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

Goal state after:
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A

pp: case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * J = J * -A → Aᵀ * u • J = u • J * -A

Tactic:
<;>

Goal state after:
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A

case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * J = J * -A → Aᵀ * u • J = u • J * -A
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
this : ∀ (m : ↥E), ∃ n, ((toEnd K (↥U) L) y' ^ n) ↑m = 0
z : L
hz : z ∈ ↑Ex
⊢ ∃ n, ((ad K L) y ^ n) z = 0

Tactic:
exact this ⟨z, hz⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y

pp: case inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y

Tactic:
<;>

Goal state after:
case inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y

case inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
<;>

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
<;>

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = 1 (Sum.inl x) y

pp: case inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = 1 (Sum.inr x) y

Tactic:
<;>

Goal state after:
case inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = 1 (Sum.inl x) y

case inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = 1 (Sum.inr x) y
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
<;>

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
<;>

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inl.inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
j₃ : l
⊢ 0 = 0 PUnit.unit (Sum.inl j₃)

pp: case inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ 0 = 0 PUnit.unit (Sum.inr val✝)

pp: case inl.inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ : l
⊢ 0 = 0 (Sum.inl i₃) PUnit.unit

pp: case inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ 0 = 0 (Sum.inr val✝) PUnit.unit

Tactic:
<;>

Goal state after:
case inl.inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
j₃ : l
⊢ 0 = 0 PUnit.unit (Sum.inl j₃)

case inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ 0 = 0 PUnit.unit (Sum.inr val✝)

case inl.inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ : l
⊢ 0 = 0 (Sum.inl i₃) PUnit.unit

case inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ 0 = 0 (Sum.inr val✝) PUnit.unit
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R
      ↥(Submodule.map (LinearMap.funLeft R R r)
          (Submodule.map A.mulVecLin (↑(LinearEquiv.funCongrLeft R R (Equiv.refl n).symm)).range)) ≤
    finrank R ↥A.mulVecLin.range

Tactic:
LinearEquiv.range,

Goal state after:
case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R r) (Submodule.map A.mulVecLin ⊤)) ≤ finrank R ↥A.mulVecLin.range
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
⊢ finrank R
      ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm))
          (Submodule.map A.mulVecLin (↑(LinearEquiv.funCongrLeft R R en)).range)) =
    finrank R ↥A.mulVecLin.range

Tactic:
LinearEquiv.range,

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
⊢ finrank R ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm)) (Submodule.map A.mulVecLin ⊤)) =
    finrank R ↥A.mulVecLin.range