mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c, L (a * a) + L (a * b) + L (a * c) + (L (b * a + b * b) + L (b * c)) + L (c * a + c * b + c * c)⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Tactic:
map_add

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (b * a) + L (b * b) + L (b * c)) + L (c * a + c * b + c * c)⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (b * a) + L (b * b) + L (b * c)) + L (c * a + c * b + c * c)⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Tactic:
map_add

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (b * a) + L (b * b) + L (b * c)) + (L (c * a + c * b) + L (c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (b * a) + L (b * b) + L (b * c)) + (L (c * a + c * b) + L (c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Tactic:
map_add

Goal state after:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L a + L b + L c,
      L (a * a) + L (a * b) + L (a * c) + (L (b * a) + L (b * b) + L (b * c)) + (L (c * a) + L (c * b) + L (c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
h : x ∈ f.ker
hx : x ∈ I
⊢ f x = 0

Tactic:
rw [mem_ker] at h

Goal state after:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
h : f x = 0
hx : x ∈ I
⊢ f x = 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⨅ i, ↑(p i)

Tactic:
by
  rw [iInf, sInf_toSubmodule]; ext; simp

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

Goal state before:
pp: case right
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ N' ≤ N ⊔ N'

Tactic:
exact le_sup_right

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ IsLieAbelian ↥(lieSpan R L s) ↔ ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0

Tactic:
by
  refine ⟨fun h x hx y hy ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
  · let x' : lieSpan R L s := ⟨x, subset_lieSpan hx⟩
    let y' : lieSpan R L s := ⟨y, subset_lieSpan hy⟩
    suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff] using this
    simp [trivial_lie_zero]
  · induction hx using lieSpan_induction with
    | mem w hw =>
      induction hy using lieSpan_induction with
      | mem u hu => simpa [Subtype.ext_iff] using h w hw u hu
      | zero => simp [Subtype.ext_iff]
      | add u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢
        simp [hu, hv]
      | smul t u _ hu =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
        simp [Subtype.ext_iff, hu]
      | lie u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
        rw [leibniz_lie]
        simp [hu, hv]
    | zero => simp [Subtype.ext_iff]
    | add u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] at hu hv ⊢
      simp [hu, hv]
    | smul t u _ hu =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
      simp [Subtype.ext_iff, hu]
    | lie u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
      simp [hu, hv]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
p : (x : M) → x ∈ lieSpan R L s → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ lieSpan R L s), p x hx → p (a • x) ⋯
x : M
lie : ∀ (x : L) (y : M) (hy : y ∈ lieSpan R L s), p y hy → p ⁅x, y⁆ ⋯
hx : x ∈ lieSpan R L s
⊢ p x hx

Tactic:
let p : LieSubmodule R L M :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩
      lie_mem := fun ⟨_, hpy⟩ ↦ ⟨_, lie _ _ _ hpy⟩ }
  exact lieSpan_le (N := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id

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

Goal state before:
pp: case right
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ J ≤ I ⊔ J

Tactic:
exact le_sup_right

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆

Tactic:
have h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆ := by
    rw [sup_le_iff]; constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_right]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
hx : (Polynomial.aeval x) p = 0
⊢ p = p * C (p.leadingCoeff⁻¹ * p.leadingCoeff)

Tactic:
inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero),

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
hx : (Polynomial.aeval x) p = 0
⊢ p = p * C 1
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
⊢ x +ᵥ ↑U ⊆ y +ᵥ ↑U ↔ x - y ∈ U

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x +ᵥ ↑U ⊆ y +ᵥ ↑U
⊢ x - y ∈ U

case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ x +ᵥ ↑U ⊆ y +ᵥ ↑U
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h✝ : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
h : (1 - p - X * q).coeff 0 = 0
⊢ I = ⊤

Tactic:
simpa [h, Ideal.eq_top_iff_one]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (p q : (R ⧸ I)[X]),
    (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) p) =
        p →
      (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) q) =
          q →
        (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (p + q)) =
          p + q

Tactic:
intro p

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : (R ⧸ I)[X]
⊢ ∀ (q : (R ⧸ I)[X]),
    (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) p) =
        p →
      (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) q) =
          q →
        (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (p + q)) =
          p + q
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (p q : R[X]),
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            (Quot.mk (⇑(Submodule.quotientRel (map C I))) p)) =
        Quot.mk (⇑(Submodule.quotientRel (map C I))) p →
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) q)) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) q →
        (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q))) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q)

Tactic:
intro p

Goal state after:
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p : R[X]
⊢ ∀ (q : R[X]),
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            (Quot.mk (⇑(Submodule.quotientRel (map C I))) p)) =
        Quot.mk (⇑(Submodule.quotientRel (map C I))) p →
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) q)) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) q →
        (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q))) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p q : MvPolynomial σ (R ⧸ I)),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
              (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
          q →
        (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
              (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p + q)) =
          p + q

Tactic:
intro p

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
⊢ ∀ (q : MvPolynomial σ (R ⧸ I)),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
              (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
          q →
        (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
              (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p + q)) =
          p + q
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p : MvPolynomial σ (R ⧸ I)) (n : σ),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X n)) =
        p * X n

Tactic:
intro p

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
⊢ ∀ (n : σ),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X n)) =
        p * X n
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
          (Ideal.Quotient.mk (Ideal.map C I)) q →
        eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          (Ideal.Quotient.mk (Ideal.map C I)) (p + q)

Tactic:
intro p

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
          (Ideal.Quotient.mk (Ideal.map C I)) q →
        eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          (Ideal.Quotient.mk (Ideal.map C I)) (p + q)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        (Ideal.Quotient.mk (Ideal.map C I)) (p * X n)

Tactic:
intro p

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
⊢ ∀ (n : σ),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        (Ideal.Quotient.mk (Ideal.map C I)) (p * X n)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

Tactic:
refine ⟨fun h p hp hp' ↦ hp.not_isUnit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩
  have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)
  obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀
  exact h p irr ((mul_dvd_mul dvd dvd).trans hd)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (1 * N).det = N.det

Tactic:
Matrix.one_mul

Goal state after:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ N.det = N.det
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
⊢ LinearMap.det 0 = 0 ^ finrank A M

Tactic:
by
  simp only [← zero_smul A (1 : M →ₗ[A] M), det_smul, mul_one, map_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : End R M
f' : End R M'
⊢ LinearMap.det (prodMap f f') = LinearMap.det f * LinearMap.det f'

Tactic:
let b := Module.Free.chooseBasis R M
  let b' := Module.Free.chooseBasis R M'
  rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
    det_fromBlocks_zero₂₁, det_toMatrix]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: K : Type u_5
V : Type u_6
W : Type u_7
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup W
inst✝² : Module K W
F : Type u_8
inst✝¹ : EquivLike F (End K V) (End K W)
inst✝ : AlgEquivClass F K (End K V) (End K W)
f : F
x : End K V
w✝ : V ≃ₗ[K] W
h : ↑f = LinearEquiv.conjAlgEquiv K w✝
⊢ ?m.70

Tactic:
by simpa using congr($h x)

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ Commute ((ad R A) a) ((ad R A) b)

Tactic:
by
  rw [Commute, SemiconjBy, ← sub_eq_zero, ← Ring.lie_def,
    ← (LieAlgebra.ad R A).map_lie, Ring.lie_def, sub_eq_zero.mpr h, map_zero]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ ∀ (a : R), (of f) a = 0 → a = 0

Tactic:
intro p

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
⊢ (of f) p = 0 → p = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
g : G
v : ι → M
⊢ (g • e).det v = e.det (g⁻¹ • v)

Tactic:
by
  simp_rw [det_apply, toMatrix_smul_left]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (x i)).degree < g.degree

Tactic:
· simp_rw [← C_mul_X_pow_eq_monomial]
            exact (degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _

Goal state after: