mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ y * x + i * 1 = 1

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ Function.Injective
    ⇑(↑R (linearCombination S c) ∘ₗ mapRange.linearMap (linearCombination R b) ∘ₗ ↑(curryLinearEquiv R))

Tactic:
simpa using! Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
by
  apply le_antisymm
  · calc
      #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
      _ = #(α × β) := mk_finset_of_infinite _
      _ = max (lift.{v} #α) (lift.{u} #β) := by
        rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
  · apply max_le <;> rw [← lift_id #(α →₀ β), ← lift_umax]
    · obtain ⟨b, hb⟩ := exists_ne (0 : β)
      exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
    · inhabit α
      exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
s : Multiset α
⊢ (fun f ↦ Finsupp.toMultiset f)
      ((fun s ↦ { support := s.toFinset, toFun := fun a ↦ count a s, mem_support_toFun := ⋯ }) s) =
    s

Tactic:
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk,
    Multiset.toFinset_sum_count_nsmul_eq]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h : ↑I ⊆ ↑J
x y : R
r : ({ toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I) x y
⊢ ({ toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J) x y

Tactic:
rw [rel_iff] at r ⊢; exact h r

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
x : M
this : ∀ (x : M), x = e.symm x • e 1
⊢ e.symm x • u (e 1) = e.symm x • e.symm (u (e 1)) • e 1

Tactic:
← this

Goal state after:
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
x : M
this : ∀ (x : M), x = e.symm x • e 1
⊢ e.symm x • u (e 1) = e.symm x • u (e 1)
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ I = ⊥ ∨ I = ⊤

Tactic:
or_iff_not_imp_left,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ ¬I = ⊥ → I = ⊤
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
x : S
hx : x ∈ s
⊢ 1 * x ∈ s

Tactic:
simpa

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

Goal state before:
pp: case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
List.map_cons,

Goal state after:
case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (hd.prod :: List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod

Tactic:
rcases ih HL.2 with ⟨z, r, hr, hzr⟩

Goal state after:
case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b c : A
hc : c ∈ R[b]
h : Commute a b
⊢ ∀ b_1 ∈ {b}, Commute a b_1

Tactic:
simpa

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

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
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
⊢ ∀ b_1 ∈ {b}, Commute a b_1

Tactic:
simpa

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ map f (adjoin R (⇑f ⁻¹' {0})) ≤ map f S

Tactic:
f.map_adjoin

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (⇑f '' ⇑f ⁻¹' {0}) ≤ map f S
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
b : κ →₀ M
h : (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = 0
this : DecidableEq κ
⊢ (equivFinsuppOfBasisRight 𝒞).symm b = (equivFinsuppOfBasisRight 𝒞).symm 0

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
b : ι →₀ N
h : (b.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = 0
this : DecidableEq ι
⊢ (equivFinsuppOfBasisLeft ℬ).symm b = (equivFinsuppOfBasisLeft ℬ).symm 0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ⅟2 • (star x + x) = ⅟2 • (x + star x)

Tactic:
add_comm

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ⅟2 • (x + star x) = ⅟2 • (x + star x)
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b.repr ((b.prod b') (Sum.inr i)).1 = b.repr 0

Tactic:
ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, Finsupp.fst_sumFinsuppLEquivProdFinsupp,
      map_zero, Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inl_ne_inr

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Embedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCancelCommMonoid M
inst✝¹ : AddMonoid.FG M
inst✝ : IsAddTorsionFree M
⊢ Injective ⇑(embedding M)

Tactic:
simpa [embedding] using! mk_left_injective 0

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
⊢ {p | p ∈ Submonoid.closure S ∧ Irreducible p} ⊆ S

Tactic:
refine fun x hx ↦
      Submonoid.closure_induction (s := S) (motive := fun x _ ↦ (Irreducible x → x ∈ S))
      (fun _ hx _ ↦ hx) (by simp) (fun a b _ _ ha hb h ↦ ?_) hx.1 hx.2

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
x : M
hx : x ∈ {p | p ∈ Submonoid.closure S ∧ Irreducible p}
a b : M
x✝¹ : a ∈ Submonoid.closure S
x✝ : b ∈ Submonoid.closure S
ha : Irreducible a → a ∈ S
hb : Irreducible b → b ∈ S
h : Irreducible (a * b)
⊢ a * b ∈ S
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: 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
hrS : 1 ∈ ↑S
hrirred : 1 ∉ {p | Irreducible p}
⊢ (fun S ↦ closure ↑S = ⊤) (S \ {1})

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: 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
⊢ ¬IsUnit r

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ LinearIndependent R A.row

Tactic:
← Matrix.vecMul_injective_iff

Goal state after:
R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective fun v ↦ v ᵥ* A
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
⊢ ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin = f

Tactic:
apply (Pi.basisFun R n).ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
⊢ ∀ (i : n), ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin ((Pi.basisFun R n) i) = f ((Pi.basisFun R n) i)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s = ra * ↑s'
ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)
⊢ (sa • r + ra • r') /ₒ (sa * s) = (ra • r' + ↑sa • r) /ₒ ⟨ra * ↑s', ⋯⟩

Tactic:
add_comm

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s = ra * ↑s'
ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)
⊢ (ra • r' + sa • r) /ₒ (sa * s) = (ra • r' + ↑sa • r) /ₒ ⟨ra * ↑s', ⋯⟩
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
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
c : ↥M
hc : ↑c * x = ↑c * y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
exact ⟨⟨c, h₁ c.2⟩, hc⟩

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
x : R
y : ↥M
z₁ z₂ : S
⊢ mk' S x y + z₁ = z₂ ↔ mk' S x y * (algebraMap R S) ↑y + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y

Tactic:
← IsUnit.mul_left_inj (IsLocalization.map_units S y),

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 : R
y : ↥M
z₁ z₂ : S
⊢ (mk' S x y + z₁) * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y ↔
    mk' S x y * (algebraMap R S) ↑y + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R
hS : S ≤ IsUnit.submonoid R
⊢ Algebra.algebraMapSubmonoid R S ≤ IsUnit.submonoid R

Tactic:
simpa

Goal state after:
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}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inl_map_mul 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}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
⊢ (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: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap A L₂) r / (algebraMap A L₂) s = f ((algebraMap A L₁) r) / f ((algebraMap A L₁) s)

Tactic:
IsScalarTower.algebraMap_apply A B L₁,

Goal state after:
A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap A L₂) r / (algebraMap A L₂) s =
    f ((algebraMap B L₁) ((algebraMap A B) r)) / f ((algebraMap B L₁) ((algebraMap A B) s))
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
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : R
⊢ (algEquiv N Sₙ Sₙ') ((algebraMap Rₘ Sₙ) ((algebraMap R Rₘ) x)) = (algebraMap Rₘ' Sₙ') ((algebraMap R Rₘ') x)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
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ₘ
⊢ IsLocalization (Algebra.algebraMapSubmonoid R M) Rₘ

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f✝ : A →ₐ[R] B
f : S →ₐ[R] B := f✝.comp (IsScalarTower.toAlgHom R S A)
g : S →ₐ[R] B := IsScalarTower.toAlgHom R S B
this : f.comp (algebraMap R S) = g.comp (algebraMap R S)
⊢ ∀ (r : S), (↑↑f✝.toRingHom).toFun ((algebraMap S A) r) = (algebraMap S B) r

Tactic:
suffices f = g by rwa [DFunLike.ext_iff] at this

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f✝ : A →ₐ[R] B
f : S →ₐ[R] B := f✝.comp (IsScalarTower.toAlgHom R S A)
g : S →ₐ[R] B := IsScalarTower.toAlgHom R S B
this : f.comp (algebraMap R S) = g.comp (algebraMap R S)
⊢ f = g
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ 1 ⊗ₜ[R] (f a / f b) = 1 ⊗ₜ[R] (a • 1 / f b)

Tactic:
algebraMap_eq_smul_one a

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ 1 ⊗ₜ[R] (a • 1 / f b) = 1 ⊗ₜ[R] (a • 1 / f b)
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (a • 1) ⊗ₜ[R] (1 / f b) = f a ⊗ₜ[R] (1 / f b)

Tactic:
algebraMap_eq_smul_one a

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (a • 1) ⊗ₜ[R] (1 / f b) = (a • 1) ⊗ₜ[R] (1 / f b)
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
this✝ : Semiring α := e.semiring
this : SMul R α := Equiv.smul R e
r : R
x : α
⊢ e.symm (e (e.symm ((algebraMap R β) r)) * e x) = e.symm (e x * e (e.symm ((algebraMap R β) r)))

Tactic:
simp [Algebra.commutes]

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

Goal state before:
pp: case neg
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
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • (↑ₐ s - a)⁻¹ʳ = (↑ₐ (r⁻¹ • s) - r⁻¹ • a)⁻¹ʳ

Tactic:
← h'.val_subInvSMul,

Goal state after:
case neg
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
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • (↑ₐ s - a)⁻¹ʳ = (↑h'.subInvSMul)⁻¹ʳ
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.liftBaseChange S ↑f) (x * y) = (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y

Tactic:
rw [← LinearMap.mul_apply_apply S, ← LinearMap.compr₂_apply,
        ← LinearMap.mul_apply_apply S, ← LinearMap.compl₁₂_apply]
      congr; ext; simp

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✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ ↑(y + a + a * y) = ↑0

Tactic:
simpa

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✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ ↑(a + y + y * a) = ↑0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx : x ∈ quasispectrum S a
⊢ (algebraMap R S) (f x) = x

Tactic:
by
    obtain (rfl | hx) := mem_quasispectrum_iff.mp hx
    · simpa using h₁ 0
    · exact h₂ hx

Goal state after: