mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ ↑(FreeAlgebra.ι R (x + y)) = ↑(FreeAlgebra.ι R x + FreeAlgebra.ι R y)

Tactic:
exact Quotient.sound <| RingConGen.Rel.of _ _ Rel.add

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)).sum = 0 •> x.fst ^ Nat.pred 0 •> x.snd

Tactic:
Nat.pred_zero,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)).sum = 0 •> x.fst ^ 0 •> x.snd
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
| L₂.map (α.app d) ≫ adj₂.counit.app d

Tactic:
rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
| L₂.map (((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app d
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
    (x.1 * y.1) •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)

Tactic:
add_assoc,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
    (x.1 * y.1) •> z.2 + (x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
| adj₁.unit.app c ≫ α.app (L₁.obj c)

Tactic:
rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
| adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul

Tactic:
← TensorProduct.map_comp,

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = TensorProduct.map (LinearMap.fst R A B ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
      comul

Tactic:
← TensorProduct.map_comp,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 = TensorProduct.map (LinearMap.fst R A B ∘ₗ inr R A B) (LinearMap.fst R A B ∘ₗ inr R A B) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul

Tactic:
← TensorProduct.map_comp,

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ 0 = TensorProduct.map (LinearMap.snd R A B ∘ₗ inl R A B) (LinearMap.snd R A B ∘ₗ inl R A B) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
      comul

Tactic:
← TensorProduct.map_comp,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = TensorProduct.map (LinearMap.snd R A B ∘ₗ inr R A B) (LinearMap.snd R A B ∘ₗ inr R A B) ∘ₗ comul
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd

Tactic:
simp only [snd_inv, snd_mul, fst_mul, fst_inv]
    simp only [smul_neg, smul_add]
    simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]
    obtain ha0 | ha := eq_or_ne (fst a) 0
    · simp [ha0]
    obtain hb0 | hb := eq_or_ne (fst b) 0
    · simp [hb0]
    rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]

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

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g (m₁ <• r₂) + g (r₁ •> m₂)) = f (r₁ * r₂) + g m₁ * f r₂ + f r₁ * g m₂

Tactic:
add_assoc,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g (m₁ <• r₂) + g (r₁ •> m₂)) = f (r₁ * r₂) + (g m₁ * f r₂ + f r₁ * g m₂)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
x : tsze R M
⊢ x ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)

Tactic:
← x.inl_fst_add_inr_snd_eq

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
x : tsze R M
⊢ inl x.fst + inr x.snd ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + a * b = a

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + (a * b + a * b) = a
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 1 + a + a = 1

Tactic:
add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 1 + (a + a) = 1
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
⊢ a * 0 = 0

Tactic:
cases a <;> rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ ε ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
rw [← LinearMap.lTensor_comp_rTensor, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul]

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ LinearMap.lTensor R f ∘ₗ (TensorProduct.mk R R M) 1 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0

pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
· simp [(IsLocalization.mk'_surjective (.powers r)).forall, Submonoid.mem_powers_iff,
      IsLocalization.Away.map, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * (-(y * x) + 1) ∈ M

Tactic:
← sub_eq_iff_eq_add.mpr df.symm,

Goal state after:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * (-(1 - i) + 1) ∈ M
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : ↑(jacobson (R ⧸ I)) ⊆ ↑⊥
⊢ ↑(Module.jacobson R (R ⧸ I)) ⊆ ↑⊥

Tactic:
rwa [← coe_jacobson_quotient]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
· exact htop.symm ▸ Set.mem_insert ⊤ _

Goal state after:
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
a : ↑↑s
⊢ f a * (algebraMap R (Away ↑a)) (↑a ^ N) = f a * (algebraMap R (Away ↑a)) (↑a ^ (N - n a) * ↑a ^ n a)

Tactic:
← pow_add,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
a : ↑↑s
⊢ f a * (algebraMap R (Away ↑a)) (↑a ^ N) = f a * (algebraMap R (Away ↑a)) (↑a ^ (N - n a + n a))
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ∃ a_1, (Units.map ↑f) a_1 = a

Tactic:
use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ (Units.map ↑f) ⋯.unit = a
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ (algebraMap R B) (x ^ (n - m) * x ^ m) = (algebraMap R B) (x ^ n)

Tactic:
← pow_add,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : m ≤ n
⊢ (algebraMap R B) (x ^ (n - m + m)) = (algebraMap R B) (x ^ n)
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s

Tactic:
rw [← IsLocalizedModule.smul_inj (IsScalarTower.toAlgHom R A Aₛ).toLinearMap s,
    IsLocalizedModule.mk'_cancel', Submonoid.smul_def, ← algebraMap_smul A]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ (algebraMap R A) ↑s • mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case mpr
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✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s → x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
case mpr
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✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x ↦ ↑(commonDenomOfFinset M s) • x) x ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)) ▷ (M ⊗ N) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (λ_ (M ⊗ N)).hom

Tactic:
simp only [comp_whiskerRight_assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (λ_ (𝟙_ C)).inv ▷ (M ⊗ N) ≫ (η ⊗ₘ η) ▷ (M ⊗ N) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (λ_ (M ⊗ N)).hom
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ tensorμ M N M N ▷ (M ⊗ N) ≫ (tensorμ (M ⊗ M) (N ⊗ N) M N ≫ (μ ▷ M ⊗ₘ μ ▷ N)) ≫ (μ ⊗ₘ μ) =
    (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ)

Tactic:
slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_assoc, mul_assoc, ← tensorHom_comp_tensorHom,
    ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ tensorμ M N M N ▷ (M ⊗ N) ≫
      tensorμ (M ⊗ M) (N ⊗ N) M N ≫ ((α_ M M M).hom ⊗ₘ (α_ N N N).hom) ≫ (M ◁ μ ⊗ₘ N ◁ μ) ≫ (μ ⊗ₘ μ) =
    (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ fst' = snd'

Tactic:
exact h.hom_ext heq (by simp [← cancel_epi g, ← h.w_assoc, heq])

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₂ ≫ v₁₃ = v₁₂ ≫ t.desc (h₁₂ ≫ v₁₃) h₂₃ ⋯

Tactic:
simp only [inl_desc]

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

Goal state before:
pp: case mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
x✝ : LocalizedModule S M
m : M
s : ↥S
⊢ β (Quot.mk ⇑(OreLocalization.oreEqv S M) (m, s))

Tactic:
exact h m s

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

Goal state before:
pp: R✝ : Type u_1
inst✝³² : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝³¹ : CommSemiring A✝
inst✝³⁰ : Algebra R✝ A✝
inst✝²⁹ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝²⁸ : AddCommMonoid M✝
inst✝²⁷ : Module R✝ M✝
M'✝ : Type u_4
inst✝²⁶ : AddCommMonoid M'✝
inst✝²⁵ : Module R✝ M'✝
inst✝²⁴ : Module A✝ M'✝
inst✝²³ : IsScalarTower R✝ A✝ M'✝
f : M✝ →ₗ[R✝] M'✝
T : Type u_5
B✝ : Type u_6
inst✝²² : CommSemiring T
inst✝²¹ : CommSemiring B✝
inst✝²⁰ : Algebra R✝ T
inst✝¹⁹ : Algebra T B✝
inst✝¹⁸ : Algebra R✝ B✝
inst✝¹⁷ : Algebra A✝ B✝
inst✝¹⁶ : IsScalarTower R✝ T B✝
inst✝¹⁵ : IsScalarTower R✝ A✝ B✝
R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
r : R
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map Algebra.TensorProduct.includeRight M
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
x✝ : S
⊢ (algebraMap S (S ⊗[R] B)) x✝ = (algebraMap (S ⊗[R] A) (S ⊗[R] B)) ((algebraMap S (S ⊗[R] A)) x✝)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

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

Goal state before:
pp: R✝ : Type u_1
inst✝³² : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝³¹ : CommSemiring A✝
inst✝³⁰ : Algebra R✝ A✝
inst✝²⁹ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝²⁸ : AddCommMonoid M✝
inst✝²⁷ : Module R✝ M✝
M'✝ : Type u_4
inst✝²⁶ : AddCommMonoid M'✝
inst✝²⁵ : Module R✝ M'✝
inst✝²⁴ : Module A✝ M'✝
inst✝²³ : IsScalarTower R✝ A✝ M'✝
f : M✝ →ₗ[R✝] M'✝
T : Type u_5
B✝ : Type u_6
inst✝²² : CommSemiring T
inst✝²¹ : CommSemiring B✝
inst✝²⁰ : Algebra R✝ T
inst✝¹⁹ : Algebra T B✝
inst✝¹⁸ : Algebra R✝ B✝
inst✝¹⁷ : Algebra A✝ B✝
inst✝¹⁶ : IsScalarTower R✝ T B✝
inst✝¹⁵ : IsScalarTower R✝ A✝ B✝
R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
r : R
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map Algebra.TensorProduct.includeRight M
this✝ : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
this : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
x✝ : A
⊢ ((algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom) x✝ =
    (Algebra.TensorProduct.includeRight.comp (algebraMap A B)) x✝

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Goal state after: