mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ Surjective ⇑p₂

Tactic:
← LieHom.range_eq_top,

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ p₂.range = ⊤
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k✝ : ℕ
y : ↥N
k : ℕ
⊢ y ∈ (dx ^ k).ker → ((ad R L) x ^ k) (N.subtype y) = 0

Tactic:
induction k generalizing y with

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹¹ : Finite ι₁
inst✝¹⁰ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁹ : LieRing L₁
inst✝⁸ : LieRing L₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
⊢ (Matrix.reindex eι.symm eι.symm) b₂.A = b₁.A

Tactic:
by simp [← hA]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst✝ : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ weightedTotalDegree' w φ = ↑n

Tactic:
simp only [weightedTotalDegree']

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst✝ : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ (φ.support.sup fun s ↦ ↑((weight w) s)) = ↑n
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i j : n
hj : j ≠ i
⊢ (monomial (Finsupp.single j 1)) (1 i j) = 0

Tactic:
simp only [one_apply_ne hj.symm, map_zero]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ toMvPolynomial b₁ b₂ (f + g) = toMvPolynomial b₁ b₂ f + toMvPolynomial b₁ b₂ g

Tactic:
unfold toMvPolynomial; simp only [map_add, Matrix.toMvPolynomial_add]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks 0 (-1) 1 0 * fromBlocks 0 (-1) 1 0 * (fromBlocks 0 (-1) 1 0)ᵀ = fromBlocks 0 (-1) 1 0

Tactic:
fromBlocks_multiply,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks (0 * 0 + -1 * 1) (0 * -1 + -1 * 0) (1 * 0 + 0 * 1) (1 * -1 + 0 * 0) * (fromBlocks 0 (-1) 1 0)ᵀ =
    fromBlocks 0 (-1) 1 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
⊢ fromBlocks A B C D ∈ symplecticGroup l R ↔ Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ mem_iff'.2 ?_⟩
  · have h_final : fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D)
        (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R := by
      simpa [mem_iff, fromBlocks_transpose, J, fromBlocks_multiply,
        sub_eq_add_neg] using transpose_mem h
    obtain ⟨h_eq1, h_eq2, _, h_eq3⟩ := fromBlocks_inj.1 h_final
    exact ⟨(sub_eq_zero.1 h_eq1).symm, (sub_eq_zero.1 h_eq3).symm, by grind⟩
  · simp only [fromBlocks_transpose, J, fromBlocks_multiply, mul_zero, mul_one, zero_add, mul_neg,
      add_zero, neg_mul, ← sub_eq_add_neg, fromBlocks_inj, sub_eq_zero]
    exact ⟨h.1.symm, by grind, by simpa using congr(transpose $(h.2.2)), h.2.1.symm⟩

Goal state after:
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✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)
hwin :
  lift.{max uR um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤
    lift.{max uR um₀, max uR um} (Module.rank R ↥(span R (range Aᵀ)))
⊢ lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range A.col)))) ≤ lift.{um₀, max uR um} A.cRank

Tactic:
simp_rw [← lift_umax] at hwin ⊢

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
h_eq : Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)
hwin :
  lift.{max (max uR um₀) (max uR um) um₀, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range Aᵀ)))) ≤
    lift.{max (max uR um) um₀, max uR um} (Module.rank R ↥(span R (range Aᵀ)))
⊢ lift.{max (max uR um₀) (max uR um) um₀, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range A.col)))) ≤
    lift.{max (max uR um) um₀, max uR um} A.cRank
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
⊢ ∀ (a : m), (∀ (x : m), diagonal w x = diagonal w a → w x = 0) → diagonal w a = 0

Tactic:
simp +contextual [funext_iff, diagonal]

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ d (d a) - d (d a) = 0 a

Tactic:
ring_nf

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ 0 = 0 a
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x : A) (y : L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x ⊗ₜ[R] y⁆ =
      ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x ⊗ₜ[R] y)⁆ - ⁅x ⊗ₜ[R] y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x⁆ =
        ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) x⁆ - ⁅x, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
      (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
        (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x + y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x + y)⁆ - ⁅x + y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

Tactic:
· intros _ _
            simp [LieAlgebra.ExtendScalars.bracket_tmul, tmul_sub, mul_comm]

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x⁆ =
        ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) x⁆ - ⁅x, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
      (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
        (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x + y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x + y)⁆ - ⁅x + y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ (toModule R ι L' fun i ↦ ↑(f i)) (((LieAlgebra.ad R (⨁ (i : ι), L i)) x) y) =
    ((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x)) ((toModule R ι L' fun i ↦ ↑(f i)) y)

Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]

Goal state after:
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ ((toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) x) y =
    ((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x) ∘ₗ toModule R ι L' fun i ↦ ↑(f i)) y
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f') (((LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) x) =
    ((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y))) ((toModule R ι L' f') x)

Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]

Goal state after:
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f' ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) x =
    ((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y)) ∘ₗ toModule R ι L' f') x
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
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
this : finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)
⊢ Ex ≤ ⟨engel K y, ⋯⟩

Tactic:
suffices engel K y = engel K x from this.ge

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
this : finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)
⊢ engel K y = engel K x
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
⊢ E.toKer.symm ⁅Exists.choose h (x + y), E.toKer m⁆ =
    E.toKer.symm (⁅Exists.choose h x, E.toKer m⁆ + ⁅Exists.choose h y, E.toKer m⁆)

Tactic:
← add_lie,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
⊢ E.toKer.symm ⁅Exists.choose h (x + y), E.toKer m⁆ = E.toKer.symm ⁅Exists.choose h x + Exists.choose h y, E.toKer m⁆
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x : E.L
y : ↥E.proj.ker
⊢ ⁅s (E.proj x) - x, y⁆ = 0

Tactic:
exact trivial_lie_zero E.proj.ker E.proj.ker ⟨_, (by simp [hs.eq])⟩ y

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
hu₃ : (F (x + y)).support ⊆ u
⊢ ((F (x + y)).sum fun a v ↦ a • (Φ ((F f) (-a))) v) =
    ((F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v) + (F y).sum fun a v ↦ a • (Φ ((F f) (-a))) v

Tactic:
sum_of_support_subset _ hu₃ _ (by simp),

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
hu₃ : (F (x + y)).support ⊆ u
⊢ ∑ x_1 ∈ u, x_1 • (Φ ((F f) (-x_1))) ((F (x + y)) x_1) =
    ((F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v) + (F y).sum fun a v ↦ a • (Φ ((F f) (-a))) v
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsDomain R
inst✝¹ : Module.IsTorsionFree R P
inst✝ : Nontrivial P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (algebraMap R P) ↑((equivNum h_nz) x) = I.den • ↑x

Tactic:
change Algebra.linearMap R P _ = _

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsDomain R
inst✝¹ : Module.IsTorsionFree R P
inst✝ : Nontrivial P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (Algebra.linearMap R P) ↑((equivNum h_nz) x) = I.den • ↑x
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : IsCancelMulZero M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
inst✝ : IsCancelMulZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
⊢ ↑(d ⟨1, ⋯⟩) = 1

Tactic:
let : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : IsCancelMulZero M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
inst✝ : IsCancelMulZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ ↑(d ⟨1, ⋯⟩) = 1
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
⊢ ↑(d ⟨c₁ 1, ⋯⟩) ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)

Tactic:
have c₂_def : ∀ t, c₂ t = d ⟨c₁ t, _⟩ := fun t => rfl

Goal state after:
case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
⊢ ↑(d ⟨c₁ 1, ⋯⟩) ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝ : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this✝⟩
this : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
⊢ b = ⊥

Tactic:
let : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le

Goal state after:
case refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this✝¹⟩
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
⊢ b = ⊥
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(d ⟨p, ⋯⟩) ^ multiplicity p m ∣ n

Tactic:
apply pow_image_of_prime_by_factor_orderIso_dvd hn hp d (pow_multiplicity_dvd ..)

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ I.FG

Tactic:
← coeIdeal_fg S inj I

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ (↑↑I).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
c : A
hc : c * a = y * b
⊢ (algebraMap A K) c ∈ 1

Tactic:
apply coe_mem_one

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case pos
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ I ≤ ⊥

Tactic:
← coeIdeal_le_coeIdeal K,

Goal state after:
case pos
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ ↑I ≤ ↑⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x✝ : K
hx✝¹ : x✝ ∈ span R₁ (f '' ↑s)
x y : K
hx✝ : x ∈ span R₁ (f '' ↑s)
hy✝ : y ∈ span R₁ (f '' ↑s)
hx : IsInteger R₁ (↑a' • x)
hy : IsInteger R₁ (↑a' • y)
⊢ IsInteger R₁ (↑a' • x + ↑a' • y)

Tactic:
exact IsLocalization.isInteger_add hx hy

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1.refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ ∃ y' ∈ I, (Algebra.linearMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'

Tactic:
exact ⟨x, hx, hx'⟩

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J

Tactic:
rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J