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

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
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) = (algebraMap S Sₘ) ((algebraMap R S) x)

Tactic:
by
      rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
have hs := Nat.sSup_mem hs₁ hs₂

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal
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
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ IsUnit (r • ↑ₐ (r⁻¹ • s) - a)

Tactic:
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using notMem_iff.mp h

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f (a₁ * a₂) * g (b₁ * b₂) = f a₁ * g b₁ * (f a₂ * g b₂)

Tactic:
map_mul,

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f a₁ * f a₂ * g (b₁ * b₂) = f a₁ * g b₁ * (f a₂ * g b₂)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f a₁ * f a₂ * g (b₁ * b₂) = f a₁ * g b₁ * (f a₂ * g b₂)

Tactic:
map_mul,

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f a₁ * f a₂ * (g b₁ * g b₂) = f a₁ * g b₁ * (f a₂ * g b₂)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ f y + f x + f x * f y = 0 ∧ f x + f y + f y * f x = 0

Tactic:
by simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
u : (PreQuasiregular A)ˣ
⊢ IsUnit (1 + ↑(PreQuasiregular.equiv.symm ↑u))

Tactic:
exact (Unitization.unitsFstOne_mulEquiv_quasiregular R).symm u |>.val.isUnit

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x : S ⊗[R] S
x✝¹ x✝ : S
⊢ (LinearMap.mul' R S).toFun (s • x✝¹ ⊗ₜ[R] x✝) = (RingHom.id S) s • (LinearMap.mul' R S).toFun (x✝¹ ⊗ₜ[R] x✝)

Tactic:
simp [TensorProduct.smul_tmul', mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
⊢ ∀ (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
hxi

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ ↑(K i)
⊢ ∀ (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : 0 < r
a b : A
hab : a < b
⊢ r • a < r • b

Tactic:
StarOrderedRing.pos_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a < b
⊢ r • a < r • b
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : 0 < a
r s : R
hrs : r < s
⊢ r • a < s • a

Tactic:
StarOrderedRing.pos_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r < s
⊢ r • a < s • a
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥⊤

Tactic:
rw [← Algebra.top_toSubmodule]

Goal state after:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F ↥(Subalgebra.toSubmodule ⊤)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ finrank F ↥⊤ = finrank F ↥⊤

Tactic:
rw [← Algebra.top_toSubmodule]

Goal state after:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ finrank F ↥⊤ = finrank F ↥(Subalgebra.toSubmodule ⊤)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = (ofVectorSpace K V) x

Tactic:
rw [ofVectorSpace_apply_self]

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

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ r, r • v₀ = v
⊢ 1 ≤ Module.rank K V

Tactic:
by_contra H
    rw [not_le, Cardinal.lt_one_iff] at H
    obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := V)
    have := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
    have := b.repr.toEquiv.subsingleton
    exact h (Subsingleton.elim _ _)

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀

Tactic:
le_span_singleton_iff

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀

Tactic:
le_span_singleton_iff

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝¹ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
x✝ : ↥s
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ ∃ r, r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Tactic:
exact ⟨r, by rwa [Subtype.ext_iff, coe_smul]⟩

Goal state after:
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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
⊢ comap f p = p ⊔ f.ker

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)
  obtain ⟨⟨y, hy⟩, hxy⟩ :=
    surjective_of_injective ((injective_restrict_iff h).mpr h') ⟨f x, hx⟩
  replace hxy : f y = f x := by simpa [Subtype.ext_iff] using hxy
  exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel y x⟩

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b c : FreeAlgebra R X), a * b * c = a * (b * c)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Goal state after:
case mk.mk.mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² * (Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b c : FreeAlgebra R X), a * (b + c) = a * b + a * c

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Goal state after:
case mk.mk.mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² * (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝) =
    Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b c : FreeAlgebra R X), (a + b) * c = a * c + b * c

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Goal state after:
case mk.mk.mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ (Quot.mk (Rel R X) a✝² + Quot.mk (Rel R X) a✝¹) * Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝ + Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b c : FreeAlgebra R X), a + b + c = a + (b + c)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Goal state after:
case mk.mk.mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² + Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² + (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case e_a
R✝ : Type u_1
X : Type u_2
inst✝⁷ : CommSemiring R✝
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ r • s • 1 = r • 1 * s • 1

Tactic:
← smul_one_mul

Goal state after:
case e_a
R✝ : Type u_1
X : Type u_2
inst✝⁷ : CommSemiring R✝
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ r • 1 * s • 1 = r • 1 * s • 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find ⋯ = 0
⊢ ↑(x % Nat.find ⋯) = 0

Tactic:
← Nat.mod_add_div x (Nat.find (not_forall.1 H)),

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑(x % Nat.find ⋯ + Nat.find ⋯ * (x / Nat.find ⋯)) = 0
H2 : ¬x % Nat.find ⋯ = 0
⊢ ↑(x % Nat.find ⋯) = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ 2 ≠ 0

Tactic:
← Nat.cast_two,

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ↑2 ≠ 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
⊢ valFromGraph hg ⋯ = (RingHom.id R) a • valFromGraph hg ⋯

Tactic:
have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
    have hav := valFromGraph_mem hg hsmul
    have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
    rw [Prod.smul_mk] at hav'
    exact (existsUnique_from_graph @hg hsmul).unique hav hav'

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.coeff n = 0

Tactic:
apply coeff_eq_zero_of_degree_lt

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.degree < ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ ⊥ < q.degree

Tactic:
rw [bot_lt_iff_ne_bot]

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ q.degree ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.support = ∅ ↔ ¬p = 0

Tactic:
← support_eq_empty

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.support = ∅ ↔ ¬p.support = ∅
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
⊢ p.coeff ap * q.coeff aq = 0

Tactic:
Finsupp.notMem_support_iff.1 h,

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 * 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [hq, leadingCoeff_zero, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (q - p).degree < q.degree

Tactic:
exact degree_sub_lt_left hd.symm hq0 hlc.symm

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n m : WithBot ℕ
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0

Tactic:
cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_two_iff]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

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

Goal state before:
pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
refine fun h => he ?_

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ (p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: 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
hp2 : p ^ i = 0
⊢ coeff 0 (i * p.natDegree + p.natDegree) = 0

Tactic:
coeff_zero

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
hp2 : p ^ i = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by
  induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, pow_succ, Nat.succ_mul]
    by_cases hp1 : p.leadingCoeff ^ i = 0
    · rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr
    · rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
      exact coeff_mul_degree_add_degree _ _

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

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

Tactic:
simp_rw [single_apply, Finsupp.add_apply] at h ⊢

Goal state after:
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