mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑(y₁ * y₂) * x₁) + (algebraMap R S) ↑y₁ * ((algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂) =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑(y₁ * y₂) * x₁) + (algebraMap R S) ↑y₁ * (algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ w *
          (↑g ((toLocalizationMap M S).sec z).1 *
            ↑((IsUnit.liftRight ((↑g).domRestrict M) hg) ((toLocalizationMap M S).sec z).2)⁻¹) +
        w' =
      v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ w * ↑g ((toLocalizationMap M S).sec z).1 *
          ↑((IsUnit.liftRight ((↑g).domRestrict M) hg) ((toLocalizationMap M S).sec z).2)⁻¹ +
        w' =
      v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ f.fieldRange = Subfield.closure ↑g.range

Tactic:
f.fieldRange_eq_map,

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ Subfield.map f ⊤ = Subfield.closure ↑g.range
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₁ + (rTensor M (inclusion ⋯)) y₂)

Tactic:
map_add,

Goal state after:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₁) +
      (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₂)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ (x • 1) ⊗ₜ[R] y ∈ Submodule.span A (Set.range ⇑((TensorProduct.mk R A M) 1))

Tactic:
← TensorProduct.smul_tmul'

Goal state after:
case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x • 1 ⊗ₜ[R] y ∈ Submodule.span A (Set.range ⇑((TensorProduct.mk R A M) 1))
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit ha) * (↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb)) - ↑(IsUnit.unit ha) * 1 = a - b

Tactic:
← mul_assoc,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit ha) * ↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb) - ↑(IsUnit.unit ha) * 1 = a - b
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ IsUnit x ↔ ∀ (i : ι), IsUnit (x i)

Tactic:
simp_rw [isUnit_iff_exists, funext_iff, ← forall_and]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ b, ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔ ∀ (i : ι), ∃ b, x i * b = 1 ∧ b * x i = 1
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ ⋃ i, quasispectrum R (a i)

Tactic:
simp only [quasispectrum, Set.mem_ofPred_eq, Set.mem_iUnion]

Goal state after:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ ∃ i, ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (algebraMap R C) (toProd 0).1 + φ (toProd 0).2 = 0

Tactic:
simp only [fst_zero, map_zero, snd_zero, φ.map_zero, add_zero]

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : StarAddMonoid R
inst✝³ : Star A
a : A
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
⊢ IsStarNormal ↑a ↔ IsStarNormal a

Tactic:
simp only [isStarNormal_iff, commute_iff_eq, ← inr_star, ← inr_mul, inr_injective.eq_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ star d = d

Tactic:
refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd

Goal state after:
case e_a
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
hx : IsSelfAdjoint x
d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ EqOn (⇑↑starAddEquiv) (⇑(AddMonoidHom.id R)) (range fun s ↦ star s * s)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
⊢ star c * (fun s ↦ star s * s) x * c = star c * star x * (x * c)

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
⊢ star c * star x * x * c = star c * star x * (x * c)
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mpr.add
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (y + z) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (y + z) * includeLeft x

Tactic:
map_add,

Goal state after:
case mpr.add
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ includeLeft x *
      ((Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z) =
    ((Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z) *
      includeLeft x
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2.inr
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
x : ↥f.ker
hx : x ∈ Set.range ⇑b₁
⊢ f ((Basis.mk H₁ ⋯) ⟨f.ker.subtype x, ⋯⟩) = (Finsupp.single ⟨f.ker.subtype x, ⋯⟩ 1) ⟨w, ⋯⟩

Tactic:
suffices x ≠ w by simp [this]

Goal state after:
case refine_2.inr
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
x : ↥f.ker
hx : x ∈ Set.range ⇑b₁
⊢ ↑x ≠ w
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : f * (g * i) = f * 1
⊢ g * f = 1

Tactic:
← mul_assoc,

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : f * g * i = f * 1
⊢ g * f = 1
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) (n + 1)) * a) =
    Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n) * a) + Quot.mk (Rel R X) a

Tactic:
map_add,

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + (algebraMap ℕ R) 1) * a) =
    Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n) * a) + Quot.mk (Rel R X) a
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
⊢ ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y

Tactic:
intro p x y hxy

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
p : ↑c
x : ↥(sSup (domain '' c))
y : ↥(↑p).domain
hxy : ↑x = ↑y
⊢ f x = ↑↑p y
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
exact (h (le_add_left 2 m) l).elim d

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
simp_rw [mem_domain_iff, h]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ ↑f ⟨x, hx⟩ = ↑g ⟨y, hy⟩

Tactic:
rw [image_iff]

Goal state after:
case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ g.graph
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
⊢ (a, y₂) ∈ g → y₁ = y₂

Tactic:
hy₂

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ y₁ = y₂
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
f : A →ₐ[R] B
m : M
a : A
⊢ (mapAlgHom M f) (single m a) = single m (f a)

Tactic:
classical ext; simp [single_apply, apply_ite f]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (p.coeff (d, n).1 * if (d, n).2 = n then 1 else 0) = p.coeff d

pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0

Tactic:
if_pos rfl,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ p.coeff (d, n).1 * 1 = p.coeff d

case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a : A
ha : a ∈ (coeff 1).support
⊢ degb a ≤ 0

Tactic:
Finset.mem_singleton.mp (Finsupp.support_single_subset ha)

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a : A
ha : a ∈ (coeff 1).support
⊢ degb 0 ≤ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * (X ^ n * C r)).coeff (d + n) = p.coeff d * r

Tactic:
← mul_assoc,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * X ^ n * C r).coeff (d + n) = p.coeff d * r
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ ((monomial m) a).natDegree ≤ m

Tactic:
classical
  rw [Polynomial.natDegree_monomial]
  split_ifs
  exacts [Nat.zero_le _, le_rfl]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p ^ 0).degree ≤ 0 • p.degree

Tactic:
by rw [pow_zero, zero_nsmul]; exact degree_one_le

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h : aq ∉ q.coeff.support
⊢ (if ap + aq = ap + aq then p.coeff ap * q.coeff aq else 0) = 0

Tactic:
if_pos rfl,

Goal state after:
case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h : aq ∉ q.coeff.support
⊢ p.coeff ap * q.coeff aq = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
by_cases hp1 : p.leadingCoeff ^ i = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (p + C (-a)).natDegree = p.natDegree

Tactic:
natDegree_add_C

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ p.natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * (↑(d.choose y) * y✝ ^ y) = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))

Tactic:
← mul_assoc,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * ↑(d.choose y) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * ↑(d.choose y) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))

Tactic:
← mul_assoc,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * ↑(d.choose y) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ (y + 1 - 1)
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = p.coeff n * r ^ n

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
if_pos rfl,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ p.coeff n * (r ^ n * 1) = p.coeff n * r ^ n

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : x i + y i = if a = i then n else 0
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i

Tactic:
obtain rfl | hai := Decidable.eq_or_ne a i

Goal state after:
case mp.inl
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x a + y a = if a = a then n else 0
⊢ (if a = a then x a else 0) = x a ∧ (if a = a then y a else 0) = y a

case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : x i + y i = if a = i then n else 0
hai : a ≠ i
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
⊢ ¬(X ∈ ⊥ ↔ X ∈ ⊤)

Tactic:
simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top,
        algebraMap_apply]

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
⊢ ∀ (x : R), ¬C ((algebraMap R A) x) = X