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

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : m r = 0
⊢ False

pp: case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
⊢ False

Tactic:
· obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
      simp at ha

Goal state after:
case inr
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
⊢ False
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
ha : ↑(oreDenom (↑s₁) s₂) * ↑s₁ = ra * ↑s₂
⊢ (oreDenom (↑s₁) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
generalize oreDenom (s₁ : R) s₂ = sa at *

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set (Subfield K)
⊢ (sInf s).toSubring = ⨅ t ∈ s, t.toSubring

Tactic:
by
  ext x
  simp [mem_sInf]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ toMatrix' (f ∘ₗ g) = toMatrix' f * toMatrix' g

Tactic:
suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f * LinearMap.toMatrix' g) by
    rw [this, LinearMap.toMatrix'_toLin']

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
rcases oreDivAddChar' r₂ r₃ s₂ s₃ with ⟨ra, sa, ha, q⟩

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ = ↑(fS s₂)⁻¹

Tactic:
have h₃' := Subtype.coe_eq_of_eq_mk h₃

Goal state after:
case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ = ↑(fS s₂)⁻¹
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Fintype ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
n : ℕ
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ Fintype.card (Fin n) = Fintype.card (Fin (Fintype.card ι))

Tactic:
simp only [Fintype.card_fin, ← Module.finrank_eq_card_basis bM, ← h,
      Module.finrank_eq_card_basis bN]

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
inst✝ : IsLocalization M S
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = (algebraMap R S) 0
hx : x = 0
⊢ z = 0

Tactic:
(algebraMap R S).map_zero

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
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ 0 < d

Tactic:
exact Nat.zero_lt_of_ne_zero hd

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

Goal state before:
pp: case map_units
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (y : ↥(Submonoid.map h M)), IsUnit ((algebraMap P S) ↑y)

pp: case surj
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (z : S), ∃ x, z * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1

pp: case exists_of_eq
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ {x y : P}, (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
· rintro ⟨_, ⟨y, hy, rfl⟩⟩
    convert! IsLocalization.map_units S ⟨y, hy⟩
    dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]
    exact congr_arg _ (h.symm_apply_apply _)

Goal state after:
case surj
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (z : S), ∃ x, z * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1

case exists_of_eq
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
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ {x y : P}, (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

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

Tactic:
neg_mul

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ FaithfulSMul R (FractionRing A)

Tactic:
faithfulSMul_iff_algebraMap_injective,

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑(algebraMap R (FractionRing A))
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * n) = mk' Rₘ r ⟨m, hm⟩

Tactic:
by rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]

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

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ u ⊗ₜ[R] v = (u * v) ⊗ₜ[R] 1

Tactic:
calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • b • 1 ⊗ₜ[R] 1
⊢ a ⊗ₜ[R] b = b ⊗ₜ[R] a

Tactic:
this a b,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • b • 1 ⊗ₜ[R] 1
⊢ a • b • 1 ⊗ₜ[R] 1 = b ⊗ₜ[R] a
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ Injective ⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))

Tactic:
by
  /- Morally the proof is to recognise that we can construct the map `A ⊗[R] M → M` as a
  composition of (`A`-linear) equivalences:
  ```
  A ⊗[R] M ≃  A ⊗[R] (A ⊗[A] M)
           ≃ (A ⊗[R] A) ⊗[A] M
           ≃ A ⊗[A] M
           ≃ M
  ```
  However the second equivalence above requires a version of heterogeneous tensor product
  associativity which is problematic in Mathlib because `TensorProduct.leftModule` prioritises the
  left factor in any tensor product. We therefore formalise a slightly lower level proof below. -/
  suffices ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m by
    let f : M →ₗ[R] A ⊗[R] M :=
      { toFun m := 1 ⊗ₜ m
        map_add' m n := tmul_add _ _ _
        map_smul' r m := tmul_smul _ _ _ }
    have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
      ext a m; simpa using! this a m
    exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩
  intro a m
  let f : A ⊗[R] A →ₗ[R] A ⊗[R] M := lift
    { toFun x :=
      { toFun y := x ⊗ₜ (y • m)
        map_add' := by simp [add_smul, tmul_add]
        map_smul' := by simp }
      map_add' := by intros; ext; simp [add_tmul]
      map_smul' := by intros; ext; simp [smul_tmul'] }
  simpa [f] using! congr_arg f (tmul_comm R 1 a)

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddGroupWithOne β
n : ℕ
⊢ e.invFun ↑↑n = ↑n

Tactic:
by simp only [Int.cast_natCast]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ (s ∪ star s).centralizer

Tactic:
centralizer_union,

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ s.centralizer ∩ (star s).centralizer
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
⊢ f = g

Tactic:
apply AlgHom.toLinearMap_injective

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
⊢ f.toLinearMap = g.toLinearMap
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 : A
r : Rˣ
⊢ σ (r • a) = r • σ a

Tactic:
by
  ext x
  have x_eq : x = r • r⁻¹ • x := by simp
  nth_rw 1 [x_eq]
  rw [smul_mem_smul_iff]
  constructor
  · exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
  · rintro ⟨w, _, (x'_eq : r • w = x)⟩
    simpa [← x'_eq]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u * a * ↑u⁻¹) = spectrum R a

Tactic:
suffices ∀ (b : A) (v : Aˣ), spectrum R (v * b * v⁻¹) ⊆ spectrum R b by
    refine le_antisymm (this a u) ?_
    apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
    simp [mul_assoc]
  intro a u μ hμ
  rw [spectrum.mem_iff] at hμ ⊢
  contrapose hμ
  simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit

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

Goal state before:
pp: 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
x : (Unitization R A)ˣ
hx : (↑x).toProd.1 = 1
⊢ x⁻¹ ∈ {x | (↑x).toProd.1 = 1}

Tactic:
simpa [-Units.mul_inv, hx] using congr(fstHom R A $(x.mul_inv))

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
⊢ ⨆ i, S i ≤ centralizer R ↑K ↔ K ≤ ⨅ i, centralizer R ↑(S i)

Tactic:
iSup_le_iff,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
⊢ (∀ (i : ι), S i ≤ centralizer R ↑K) ↔ K ≤ ⨅ i, centralizer R ↑(S i)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M

Tactic:
refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
⊢ #↑↑⟨s, hs⟩ + #↑↑⟨t, ht⟩ ≤ Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case hbc
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀

Tactic:
rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
    apply Cardinal.natCast_lt_aleph0

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)

Tactic:
suffices Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{v} (finrank R M : Cardinal.{w}) by
    rwa [Cardinal.lift_le] at this
  calc
    Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) :=
      hp.subtype_ne_bot_le_rank
    _ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
    _ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ NonUnitalAlgebra.adjoin R (s ∪ star s) ≤ S.toNonUnitalSubalgebra ↔ s ⊆ ↑S

Tactic:
NonUnitalAlgebra.adjoin_le_iff,

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S.toNonUnitalSubalgebra ↔ s ⊆ ↑S
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : ↑(finrank R (M ⧸ N)) + Module.rank R ↥N ≤ ↑(finrank R M)
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
← N.finrank_eq_rank

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : ↑(finrank R (M ⧸ N)) + ↑(finrank R ↥N) ≤ ↑(finrank R M)
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case a
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
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose ⋯ • x = ↑w
⊢ Classical.choose ⋯ • x = (Classical.choose ⋯ + Classical.choose ⋯) • x

Tactic:
simp only [add_smul, this, ← coe_add]

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
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥Q = Module.rank K ↥Q'

Tactic:
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'⟩]

Goal state after:
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'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ ∑ x ∈ p.support, T (g x (p.coeff x)) = p.sum fun n a ↦ T (g n a)

Tactic:
sum

Goal state after:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ ∑ x ∈ p.support, T (g x (p.coeff x)) = ∑ n ∈ p.support, T (g n (p.coeff n))
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
lift a to ℕ using le_of_lt h with b

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h : 0 < ↑b
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m

Tactic:
by_cases n1 : n = 1

Goal state after:
case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
⊢ 0 < n.minFac

Tactic:
by_cases n1 : n = 1

Goal state after:
case pos
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac

case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Tactic:
· exact ‹p.Prime›.ne_zero

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 : R[M] →ₐ[R] A
f : R[M]
| F f

Tactic:
rw [lift_unique' F]
    simp [lift_apply]

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 : R[M] →ₐ[R] A
f : R[M]
| f.coeff.sum fun a b ↦ b • F (single a 1)