mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ (quotUliftToQuot F) ((Quot.ι (F ⋙ uliftFunctor) j) { down := a }) = (Quot.ι F j) a

Tactic:
quotUliftToQuot_ι

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ (Quot.ι F j) { down := a }.down = (Quot.ι F j) a
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (c.ι.app j ≫ hc.desc (toCocone F f))) x = f ((ι F j) x)

Tactic:
rw [hc.fac]

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((toCocone F f).ι.app j)) x = f ((ι F j) x)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case mul
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ : N
a b : M
h1 : c a b
a✝¹ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f a) (f b)
p q : M
h2 : c p q
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) (f p) (f q)
⊢ Relation.Map (⇑c) (⇑f) (⇑f) (f a * f p) (f b * f q)

Tactic:
exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩

Goal state after:
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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ringCon R M ≤ RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom

Tactic:
grw [ringCon, RingCon.ringConGen_le]
        intro x y h
        induction h <;>
          simp [Algebra.smul_def, FreeAlgebra.lift_ι_apply,
            map_mul, AlgHom.commutes, map_add, RingCon.ker]

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

Goal state before:
pp: 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
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹⁻¹ = 1 * x⁻¹⁻¹

Tactic:
by rw [one_mul]

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

Goal state before:
pp: 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
x : tsze R M
hx : x.fst ≠ 0
⊢ x * (x⁻¹ * x⁻¹⁻¹) = x

Tactic:
TrivSqZeroExt.mul_inv_cancel,

Goal state after:
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
x : tsze R M
hx : x.fst ≠ 0
⊢ x * 1 = x

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
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst ≠ 0
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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) (inl R A B) ∘ₗ comul) x) =
    (TensorProduct.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) ∘ₗ comul) x

Tactic:
← map_comp_rTensor,

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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      (((TensorProduct.map (TensorProduct.map (inl R A B) (inl R A B)) (inl R A B) ∘ₗ rTensor A comul) ∘ₗ comul) x) =
    (TensorProduct.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) ∘ₗ comul) x
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
L₁ L₂ : A ⥤ B
R₁ R₂ : B ⥤ A
L : B ⥤ C
R : C ⥤ B
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
⊢ (conjugateEquiv (adj₁.comp adj) (adj₂.comp adj)) (whiskerRight τ L) = R.whiskerLeft ((conjugateEquiv adj₁ adj₂) τ)

Tactic:
by
  ext X
  simp only [comp_obj, conjugateEquiv_apply_app, comp_unit_app, Functor.whiskerRight_app,
    Functor.comp_map, comp_counit_app, ← map_comp, assoc, Functor.whiskerLeft_app]
  simp

Goal state after:
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
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) (inr R A B) ∘ₗ comul) x) =
    (TensorProduct.map (inr R A B) (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) ∘ₗ comul) x

Tactic:
← map_comp_rTensor,

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
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      (((TensorProduct.map (TensorProduct.map (inr R A B) (inr R A B)) (inr R A B) ∘ₗ rTensor B comul) ∘ₗ comul) x) =
    (TensorProduct.map (inr R A B) (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) ∘ₗ comul) x
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul

Tactic:
← map_comp_rTensor,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i) ∘ₗ rTensor (A i) comul) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
        TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul

Tactic:
← map_comp_rTensor,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
        TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i) ∘ₗ rTensor A comul) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
⊢ counit ∘ₗ DFinsupp.coeFnLinearMap R = counit

Tactic:
by
  apply LinearMap.ext fun x ↦ ?_
  have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _
  rw [← DFinsupp.sum_single (f := x)]
  simp [DFinsupp.single_eq_pi_single]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
        map (map (LinearMap.single R A i✝) (LinearMap.single R A i✝) ∘ₗ comul) (LinearMap.single R A i✝)) ∘ₗ
      comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝) ∘ₗ comul) ∘ₗ comul

Tactic:
← map_comp_rTensor,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
        map (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) (LinearMap.single R A i✝) ∘ₗ
          rTensor (A i✝) comul) ∘ₗ
      comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
rw [← leftAdjointUniq_hom_counit adj1 adj2]
  rfl

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

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

Tactic:
by cases a <;> rfl

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

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

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

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

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

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑α.toPartOrd
⊢ (Hom.hom (ofHom ↑e ≫ ofHom ↑e.symm)) a✝ = (Hom.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

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

Goal state before:
pp: α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
a✝ : ↑α.toLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

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

Goal state before:
pp: α β : HeytAlg
e : ↑α ≃o ↑β
a✝ : ↑α
⊢ (Hom.hom
        (ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
          ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }))
      a✝ =
    (Hom.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ f (⊤ \ a) = ⊤ \ f a

Tactic:
map_sdiff,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ f ⊤ \ f a = ⊤ \ f a
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingAlgebra γ
f₁ f₂ : HeytingHom α β
g : HeytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Category.BoolRing

Goal state before:
pp: α β : BoolRing
e : ↑α ≃+* ↑β
x✝ : ↑α
⊢ (Hom.hom ({ hom' := ↑e } ≫ { hom' := ↑e.symm })) x✝ = (Hom.hom (𝟙 α)) x✝

Tactic:
exact e.symm_apply_apply _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BiheytingAlgebra α
inst✝¹ : BiheytingAlgebra β
inst✝ : BiheytingAlgebra γ
f₁ f₂ : BiheytingHom α β
g : BiheytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

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)
n : ℕ
⊢ (algebraMap R S) e = (algebraMap R S) 1

Tactic:
H,

Goal state after:
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)
n : ℕ
⊢ e * e = e * 1
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ x - y ∈ RingHom.ker (algebraMap R S) ↔ e * x = e * y

Tactic:
H,

Goal state after:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ x - y ∈ Ideal.span {1 - e} ↔ e * x = e * y
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
let 𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R (S := Rᵐᵒᵖ) R (.op r)) 𝔪

Goal state after:
case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x * r ∈ 𝔪
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r

Tactic:
mem_bot,

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r - 1 = 0
⊢ IsUnit r
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
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

pp: case neg
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 : n < m
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
· rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]

Goal state after:
case neg
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 : n < m
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_3
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
⊢ (limit.π F i ≫ if h : j✝ = i then eqToHom ⋯ else (H j✝ h).from (((Functor.const J).obj (F.1 i)).obj j✝)) =
    𝟙 (limit F) ≫ limit.π F j✝

Tactic:
split_ifs with h

Goal state after:
case pos
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
h : j✝ = i
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F j✝

case neg
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
h : ¬j✝ = i
⊢ limit.π F i ≫ (H j✝ h).from (((Functor.const J).obj (F.1 i)).obj j✝) = 𝟙 (limit F) ≫ limit.π F j✝
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = b * (algebraMap R B) (x ^ d)

Tactic:
H,

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = (algebraMap R B) a₀
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(finsetIntegerMultiple M s) = commonDenomOfFinset M s • ↑s

Tactic:
delta finsetIntegerMultiple commonDenom

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
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(Finset.image (fun t ↦ integerMultiple M s id t) s.attach) = commonDenomOfFinset M s • ↑s
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ { l //
    (PushoutCocone.mk f g ⋯).inl ≫ l = s.inl ∧
      (PushoutCocone.mk f g ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
          (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl → (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = l }

Tactic:
use BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Goal state after:
case property
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ (PushoutCocone.mk f g ⋯).inl ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inl ∧
    (PushoutCocone.mk f g ⋯).inr ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
      ∀ {m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt},
        (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl →
          (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap R A)
⊢ IsPushout R T A T

Tactic:
have : IsLocalization (IsUnit.submonoid R) A :=
    IsLocalization.of_le_isUnit_of_bijective Algebra.algebraMapSubmonoid_isUnit_le_isUnit H

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap R A)
this : IsLocalization (IsUnit.submonoid R) A
⊢ IsPushout R T A T