mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a \ b) = (⇑f ∘ ⇑g) a \ (⇑f ∘ ⇑g) b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⇨ b) = (⇑f ∘ ⇑g) a ⇨ (⇑f ∘ ⇑g) b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a \ b) = (⇑f ∘ ⇑g) a \ (⇑f ∘ ⇑g) b

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ X).hom ⊗ₘ 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ₘ 𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ₘ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ 𝟙 X ⊗ₘ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).inv ⊗ₘ 𝟙 Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ₘ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom = (𝟙 W ⊗ₘ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).inv) = (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ₘ 𝟙 Z) = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X : BoolAlg
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y : BoolAlg
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y : BoolAlg
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] R
g : N →ₗ[R] M'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (λ ∘ₗ f ⊗ₘ g)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id)) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
inst✝² : MonoidalCategory C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙 (𝟙_ C) ▷ 𝟙_ C = (λ_ (𝟙_ C)).inv

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : N →ₗ[R] R
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (ρ ∘ₗ f ⊗ₘ g)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g)) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : N →ₗ[R] R
h : P →ₗ[R] M ⊗[R] N
⊢ ρ ∘ₗ f ⊗ₘ g ∘ₗ h = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g ∘ₗ h

Tactic:
by
  simp only [← LinearMap.comp_assoc, rid_comp_map f]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : ComonObj X
⊢ Δ ≫ Δ ▷ X = Δ ≫ X ◁ Δ ≫ (α_ X X X).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ (η ≫ f.hom.op).unop = η.unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ (μ ≫ f.hom.op).unop = ((f.hom.op ⊗ₘ f.hom.op) ≫ μ).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (f.unop.hom.unop ≫ ε).op = ε.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
M N O : C
inst✝⁵ : ComonObj M
inst✝⁴ : ComonObj N
inst✝³ : ComonObj O
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
A : Comon C
⊢ { hom := F.map (𝟙 A).hom, isComonHom_hom := ⋯ }.hom = (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
M N O : C
inst✝⁵ : ComonObj M
inst✝⁴ : ComonObj N
inst✝³ : ComonObj O
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X✝ Y✝ Z✝ : Comon C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ }.hom =
    ({ hom := F.map f.hom, isComonHom_hom := ⋯ } ≫ { hom := F.map g.hom, isComonHom_hom := ⋯ }).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: n : Type v
inst✝ : Unique n
X✝ Y✝ : CommRingCat
f : X✝ ⟶ Y✝
x✝ : ↑((coyoneda.obj (op n)).obj X✝)
⊢ (Hom.hom ((coyoneda.obj (op n)).map f ≫ (RingEquiv.piUnique fun i ↦ ↑Y✝).toCommRingCatIso.hom)) x✝ =
    (Hom.hom ((RingEquiv.piUnique fun i ↦ ↑X✝).toCommRingCatIso.hom ≫ (𝟭 CommRingCat).map f)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
r✝ : ↑R
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single 1 r✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m✝ : ↑X✝
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single m✝ 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case zero
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ 0 ∣ b ↔ replicate 0 (normalize a) ≤ normalizedFactors b)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬count (normalize a) (normalizedFactors b) + 1 ≤ count (normalize a) (normalizedFactors b)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case inl.zero
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
hle : 0 ^ 0 ∣ x
hlt : ¬0 ^ (0 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = 0

pp: case inl.succ
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
n✝ : ℕ
hle : 0 ^ (n✝ + 1) ∣ x
hlt : ¬0 ^ (n✝ + 1 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n✝ + 1

Tactic:
· exact count_eq_zero.2 (zero_notMem_normalizedFactors _)

Goal state after:
case inl.succ
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hnorm : normalize 0 = 0
n✝ : ℕ
hle : 0 ^ (n✝ + 1) ∣ x
hlt : ¬0 ^ (n✝ + 1 + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n✝ + 1
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
n : ℕ
⊢ (fun x_1 ↦ x ^ x_1) 1 = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (fun x_1 ↦ x ^ x_1) 1 = x

Tactic:
simp

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

Goal state before:
pp: case h
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
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
n : ℕ
⊢ (fun x ↦ f r ^ x) n = f ((fun x ↦ r ^ x) n)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.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
P : Type u_3
inst✝¹⁷ : CommSemiring P
x : R
inst✝¹⁶ : Away x S
g : R →+* P
Q : Type u_4
inst✝¹⁵ : CommSemiring Q
inst✝¹⁴ : Algebra P Q
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ ↑↑(IsLocalization.map Bₚ ↑f ⋯) ((algebraMap A Aₚ) ((algebraMap R A) r)) = ((algebraMap B Bₚ).comp (algebraMap R B)) r

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x : R
hx : x ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x✝ : x - 0 ∈ span s
⊢ p (x - 0) x✝ → p x hx

Tactic:
simp

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

Goal state before:
pp: case e'_3
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x✝ y : R
inst✝² : Away x✝ S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x✝) T
x : S₁
⊢ x ∈ Submonoid.powers ((algebraMap R S₁) y) ↔ x ∈ Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : R
⊢ (algebraMap R S) z * (algebraMap R S) ↑(z, 1).2 = (algebraMap R S) (z, 1).1

Tactic:
simp

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

Goal state before:
pp: case fst
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✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := ⋯
⊢ ((1, 0) * (1, 0)).1 = (1, 0).1

Tactic:
simp

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

Goal state before:
pp: case snd
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✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := ⋯
⊢ ((1, 0) * (1, 0)).2 = (1, 0).2

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.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✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
x✝¹ x✝ : R × S
xR : R
xS : S
yR : R
yS : S
⊢ xR = yR ↔ (1, 0) * (xR, xS) = (1, 0) * (yR, yS)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) (1 * x) 1 = x

Tactic:
simp

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

Goal state before:
pp: case fst
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✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := ⋯
⊢ ((0, 1) * (0, 1)).1 = (0, 1).1

Tactic:
simp

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

Goal state before:
pp: case snd
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✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := ⋯
⊢ ((0, 1) * (0, 1)).2 = (0, 1).2

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.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✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := (RingHom.snd R S).toAlgebra
x✝¹ x✝ : R × S
xR : R
xS : S
yR : R
yS : S
⊢ xS = yS ↔ (0, 1) * (xR, xS) = (0, 1) * (yR, yS)

Tactic:
simp

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

Goal state before:
pp: S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
s : S
⊢ ∃ a, (algebraMap S T) s * (algebraMap S T) r ^ 0 = (algebraMap S T) a

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R
x✝ : R
h : ∀ (I : TwoSidedIdeal R), ↑J ⊆ ↑I → x✝ ∈ I
x : R
⊢ x ∈ ↑J → x ∈ ↑(mk' ↑J ⋯ ⋯ ⋯ ⋯ ⋯)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ (TwoSidedIdeal.asIdeal I).toTwoSided ↔ x✝ ∈ I

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ TwoSidedIdeal.asIdeal I.toTwoSided ↔ x✝ ∈ I

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x✝ : TwoSidedIdeal R
⊢ (fun I ↦
        have this := ⋯;
        (↑I).toTwoSided)
      ((fun I ↦ ⟨asIdeal I, ⋯⟩) x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : { I // I.IsTwoSided }
⊢ (fun I ↦ ⟨asIdeal I, ⋯⟩)
      ((fun I ↦
          have this := ⋯;
          (↑I).toTwoSided)
        I) =
    I

Tactic:
simp

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

Goal state before:
pp: case refine_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ IsUnit ((algebraMap S T) ((algebraMap R S) r))

Tactic:
rwa [← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
x✝ : R
⊢ r = r - 1 + 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
⊢ 0 ∈ nonunits R

Tactic:
simp

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

Goal state before:
pp: case refine_1
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
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
refine
      sInf_le_sInf fun J hJ =>
        ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, ?_⟩, map_comap_of_surjective f hf J⟩⟩

Goal state after:
case refine_1
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 ∈ {J | map f I ≤ J ∧ J.IsMaximal}
⊢ (comap f J).IsMaximal
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set 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
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
⊢ ↑({↑a} ∪ t) = {↑a} ∪ ↑t

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Instances

Goal state before:
pp: R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit ((CommRingCat.Hom.hom f.hom) a)
⊢ a = (CommRingCat.Hom.hom f.inv) ((CommRingCat.Hom.hom f.hom) a)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : X = i then eqToHom ⋯ else (H X h).from (((Functor.const J).obj (F.1 i)).obj X)) ≫ F.map f

Tactic:
intro j

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
⊢ ∀ ⦃Y : J⦄ (f : j ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j)) ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.1 i)).map (𝟙 i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ F.map (𝟙 i)

Tactic:
simp

Goal state after: