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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((r • s) • x) = r • (addEquiv R S M).symm (s • x)

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm (((algebraMap R S) r * s) • x) = r • (addEquiv R S M).symm (s • x)
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
inst✝¹ : IsLocalization M S
inst✝ : Finite R
x : S
⊢ ∃ a, uncurry (mk' S) a = x

Tactic:
by
    simpa using IsLocalization.exists_mk'_eq M x

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂

Tactic:
rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.domRestrict M) h y),
    mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
    IsUnit.coe_liftRight]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ((↑g).domRestrict M) y * z₁ = ((↑g).domRestrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
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
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) (z • x) = g z • (map Q g hy) x

Tactic:
Algebra.smul_def,

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
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) ((algebraMap R S) z * x) = g z • (map Q g hy) x
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
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) ((algebraMap R S) z * x) = g z • (map Q g hy) x

Tactic:
Algebra.smul_def,

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
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) ((algebraMap R S) z * x) = (algebraMap P Q) (g z) * (map Q g hy) x
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
replace Ha : (a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsFractionRing R R ↔ Function.Surjective ⇑(algebraMap R K)

Tactic:
by
  rw [self_iff_bijective K, Function.Bijective, and_iff_right (IsFractionRing.injective R K)]

Goal state after:
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map h M) S

Tactic:
refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩

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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ IsLocalization (Submonoid.map h M) S → IsLocalization M S
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ star q * star p = p ↔ p * q = p

Tactic:
rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm]

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p = p * q ∧ p = p * q ↔ p = p * q
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ˣ
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)

Tactic:
by
  have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) := by
    refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
    · calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
    · calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
  have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
  rw [mul_smul_comm r⁻¹ b a] at this
  simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def,
    IsUnit.smul_sub_iff_sub_inv_smul, smul_mul_assoc]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} - σ a = σ (↑ₐ r - a)

Tactic:
by
  rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ adjoin R (⇑(map f g) '' {t | ∃ a b, a ⊗ₜ[R] b = t}) ≤ (includeLeft.comp f).range ⊔ (includeRight.comp g).range

Tactic:
adjoin_le_iff

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ ⇑(map f g) '' {t | ∃ a b, a ⊗ₜ[R] b = t} ⊆ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (algebraMap R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ Subalgebra.map (lmul' R) (includeLeft.comp f).range ⊔ Subalgebra.map (lmul' R) (includeRight.comp g).range =
    f.range ⊔ g.range

Tactic:
← AlgHom.range_comp,

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ ((lmul' R).comp (includeLeft.comp f)).range ⊔ Subalgebra.map (lmul' R) (includeRight.comp g).range = f.range ⊔ g.range
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ ((lmul' R).comp (includeLeft.comp f)).range ⊔ Subalgebra.map (lmul' R) (includeRight.comp g).range = f.range ⊔ g.range

Tactic:
← AlgHom.range_comp,

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ ((lmul' R).comp (includeLeft.comp f)).range ⊔ ((lmul' R).comp (includeRight.comp g)).range = f.range ⊔ g.range
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
⊢ ∃ g, g ∘ₗ f = id

Tactic:
by
  let B := Basis.ofVectorSpaceIndex K V
  let hB := Basis.ofVectorSpace K V
  have hB₀ : _ := hB.linearIndependent.linearIndepOn_id
  have : LinearIndepOn K _root_.id (f '' B) := by
    have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
    rwa [Basis.range_ofVectorSpace K V] at h₁
  let C := this.extend (subset_univ _)
  have BC := this.subset_extend (subset_univ _)
  let hC := Basis.extend this
  have Vinh : Inhabited V := ⟨0⟩
  refine ⟨(hC.constr ℕ : _ → _) (C.domRestrict (invFun f)), hB.ext fun b => ?_⟩
  rw [image_subset_iff] at BC
  have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
    change f b = Basis.extend this _
    simp_rw [Basis.extend_apply_self]
  dsimp
  rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
  exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x₁ : M
x₁_mem' : x₁ ∈ t.erase x₀
x₁_mem : shift x₁ ∈ t'
nz : g (shift x₁) ≠ 0
this : x₁ ≠ x₀ ∧ x₁ ∈ t
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
change (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
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
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
⊢ ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x

Tactic:
by
  obtain ⟨Q, hQ⟩ := Submodule.exists_isCompl W
  let eQ := W.prodEquivOfIsCompl Q hQ
  obtain ⟨Q', hQ'⟩ := Submodule.exists_isCompl W'
  let eQ' := W'.prodEquivOfIsCompl Q' hQ'
  suffices Nonempty (Q ≃ₗ[K] Q') from
    ⟨eQ.symm ≪≫ₗ (LinearEquiv.prodCongr f this.some) ≪≫ₗ eQ', by aesop⟩
  refine Module.nonempty_linearEquiv_iff_rank_eq.mpr ?_
  rw [← Cardinal.add_right_inj_of_lt_aleph0 (γ := Module.rank K W),
    add_comm, ← rank_prod', Module.nonempty_linearEquiv_iff_rank_eq.mp ⟨eQ⟩,
    add_comm, Module.nonempty_linearEquiv_iff_rank_eq.mp ⟨f⟩,
    ← rank_prod', Module.nonempty_linearEquiv_iff_rank_eq.mp ⟨eQ'⟩]
  exact Module.rank_lt_aleph0 K ↥W

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
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f ↔ f.range = ⊤

Tactic:
rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ⇑g ∘ ι R = f ↔ g = (lift R) f

Tactic:
rw [← (lift R).symm_apply_eq, lift]

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ⇑g ∘ ι R = f ↔ { toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm g = f
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr
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 : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1

Tactic:
use f ⟨x, h⟩
    simp only [h, exists_const]

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharP R 1
⊢ False

Tactic:
have : Subsingleton R := CharOne.subsingleton

Goal state after:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharP R 1
this : Subsingleton R
⊢ False
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mpr
n : ℕ
h : 2 ∣ n
⊢ n.minFac = 2

Tactic:
have ub := minFac_le_of_dvd (le_refl 2) h

Goal state after:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
⊢ n.minFac = 2
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2

Tactic:
· intro h
    have ub := minFac_le_of_dvd (le_refl 2) h
    have lb := minFac_pos n
    refine ub.eq_or_lt.resolve_right fun h' => ?_
    suffices n.minFac = 1 by simp_all
    exact (le_antisymm (Nat.succ_le_of_lt lb) (Nat.lt_succ_iff.mp h')).symm

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Subsingleton M
a : A
⊢ (uniqueAlgEquiv R M).symm a = single 1 a

Tactic:
by ext; simp [uniqueAlgEquiv]

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : M →* A
a : M
b : R
⊢ ↑(algebraMap R A) b * F a = b • F a

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : M →* A
a : M
b : R
⊢ ↑(algebraMap R A) b * F a = (algebraMap R A) b * F a
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₀ ⟨hx, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx)) g₀

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (erase p.natDegree p).degree < p.degree

Tactic:
apply lt_of_le_of_ne (degree_erase_le _ _)
  rw [degree_eq_natDegree hp, degree, support_erase]
  exact fun h => notMem_erase _ _ (mem_of_max h)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ #(range (p.natDegree + 1))

Tactic:
exact Finset.card_le_card supp_subset_range_natDegree_succ

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
h : 0 ≠ 1
p : R[X]
hp : p.Monic
inst✝ : Nontrivial R
⊢ p ≠ 0

Tactic:
exact hp.ne_zero

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]

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:
by
  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.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
⊢ q = 0

Tactic:
by
  by_contra hc
  exact lt_iff_not_ge.mp h₂ (natDegree_le_of_dvd h₁ hc)

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

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

Tactic:
by rw [pow_zero, ← C_1] at *; rw [degree_C h, zero_nsmul]

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.leadingCoeff ^ n * p.leadingCoeff ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
← leadingCoeff_pow' h₁

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
⊢ Function.invFun D (supDegree D p) ∈ p.coeff.support

Tactic:
obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D hp

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ Function.invFun D (supDegree D p) ∈ p.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ Function.invFun D (supDegree D p) ∈ p.coeff.support

Tactic:
he,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ Function.invFun D (D a) ∈ p.coeff.support
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b).degree < (C a * X).degree

Tactic:
by
  simpa only [degree_C_mul_X ha] using degree_C_lt

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff 0 * 0 ^ 0 = eval 0 p

Tactic:
by
      symm
      rw [eval_eq_sum]
      exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow hb]) (by simp)

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

Goal state before:
pp: S : Type v
inst✝ : Semiring S
c : S
⊢ (X + C c).nextCoeff = c

Tactic:
nontriviality S

Goal state after:
S : Type v
inst✝ : Semiring S
c : S
a✝ : Nontrivial S
⊢ (X + C c).nextCoeff = c
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n

Tactic:
Finset.mem_range_succ_iff,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : ¬n ≤ p.natDegree
⊢ p.natDegree < n
Module: Mathlib.Algebra.Order.Pi

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

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

Goal state before:
pp: case refine_4
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f (comapDomain (⇑f) v ⋯) = v

Tactic:
embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))

Goal state after:
case refine_4
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ v = v