mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
set K : Set (M × M) := (insert 0 (range f)) ×ˢ (insert 0 (range g))

Goal state after:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ IsClosed[inst✝²] s.centralizer

Tactic:
rw [centralizer, ofPred_forall]

Goal state after:
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ IsClosed[inst✝²] (⋂ i, {x | i ∈ s → i * x = x * i})
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ F * closure[inst✝²] {1} = closure[inst✝²] F * closure[inst✝²] {1}

Tactic:
hF.closure_eq

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ F * closure[inst✝²] {1} = F * closure[inst✝²] {1}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
simp_rw [Set.mem_ofPred, id]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ hg
  filter_upwards [hg.eventually (eventually_ge_atTop 0),
    hf.eventually (eventually_ge_atTop 1)] with _ using le_mul_of_one_le_left

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ IsUniformGroup G

Tactic:
by
  constructor
  have : (fun (x : (G × G) × (G × G)) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) =
    (fun (p : G × G) ↦ p.1 * p.2⁻¹)
      ∘ (fun (p : (G × G) × (G × G)) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) := by
    ext x
    simp only [Function.comp_apply, mul_inv_rev, inv_inv]
    rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]
    simp [mul_assoc]
  simp only [UniformContinuous, div_eq_mul_inv, uniformity_prod_eq_prod,
    uniformity_eq_comap_nhds_one', prod_comap_comap_eq, ← nhds_prod_eq, tendsto_comap_iff,
    Function.comp_def, mul_inv_rev, inv_inv, tendsto_map'_iff]
  rw [this]
  apply Tendsto.comp ?_ tendsto_comap
  nth_rewrite 3 [show (1 : G) = 1 * 1⁻¹ by simp]
  apply Continuous.tendsto (by fun_prop)

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto Inv.inv (map (fun x_1 ↦ x * x_1) (𝓝 1)) (𝓝 x⁻¹)

Tactic:
← nhds_translation_mul_inv₀ hx',

Goal state after:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto Inv.inv (map (fun x_1 ↦ x * x_1) (𝓝 1)) (comap (fun x_1 ↦ x_1 * x⁻¹⁻¹) (𝓝 1))
Module: Mathlib.Topology.Order.LocalExtr

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : Preorder β
f : α → β
a : α
⊢ IsLocalMaxOn f univ a ↔ IsLocalMax f a

Tactic:
simp only [IsLocalMaxOn, IsLocalMax, nhdsWithin_univ]

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ico (f i) b = Ico f (update f i b)

Tactic:
by simpa using image_update_Ico f i (f i) b

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, ts] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)

Tactic:
simp_rw +instances [OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff]
  aesop

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯)) =
    (ConcreteCategory.hom F'.m) 0

Tactic:
change (F'.e ≫ F'.m) _ = _

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) =
    (ConcreteCategory.hom F'.m) 0
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x

Tactic:
change (F'.e ≫ F'.m) _ = _

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : IsMax a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h :
  (Submodule.liftQSpanSingleton (↑(addOrderOf a))
        (AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a))) ⋯)
      (↑(intSpanEquivQuotAddOrderOf a) ⟨a, ⋯⟩) =
    0
⊢ a = 0

Tactic:
intSpanEquivQuotAddOrderOf_apply_self,

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h :
  (Submodule.liftQSpanSingleton (↑(addOrderOf a))
        (AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a))) ⋯)
      (Submodule.Quotient.mk 1) =
    0
⊢ a = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
h : a < x ∧ x < a + p
⊢ liftIoc p a f ↑x = f x

Tactic:
· exact liftIoc_coe_apply ⟨h.1, h.2.le⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
A' : C
π : A' ⟶ A
hπ : Epi π
x : A' ⟶ X
fac : π ≫ y = x ≫ f
⊢ y ≫ Cofork.π c = 0

Tactic:
simp [← cancel_epi π, reassoc_of% fac, condition]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
← w ⟨WalkingPair.left⟩,

Goal state after:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R (↑M × ↑N),
        π :=
          {
            app := fun j ↦
              Discrete.casesOn j fun j ↦ WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
            naturality := ⋯ } }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R (↑M × ↑N),
                π :=
                  {
                    app := fun j ↦
                      Discrete.casesOn j fun j ↦
                        WalkingPair.casesOn j (↟(LinearMap.fst R ↑M ↑N)) (↟(LinearMap.snd R ↑M ↑N)),
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ m = ↟((Hom.hom (m ≫ ↟(LinearMap.fst R ↑M ↑N))).prod (Hom.hom (s.π.app { as := WalkingPair.right })))
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ T.δ.app X.A ≫ T.ε.app (T.obj X.A)

Tactic:
Comonad.left_counit

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ 𝟙 (T.obj X.A)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
i : Fin (0 + 1)
⊢ φ.app i = φ'.app i

Tactic:
fin_cases i

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ φ.app ((fun i ↦ i) ⟨0, ⋯⟩) = φ'.app ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
f : F ⟶ G
x✝ : IsIso (f.app 0)
i : Fin (0 + 1)
⊢ IsIso (f.app i)

Tactic:
fin_cases i

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
f : F ⟶ G
x✝ : IsIso (f.app 0)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
f : F ⟶ G
x✝ : IsIso (f.app 0)
i : Fin (0 + 1)
⊢ IsIso (f.app i)

Tactic:
by fin_cases i; assumption

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
i : Fin (1 + 1)
⊢ IsIso (f.app i)

Tactic:
fin_cases i

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ F.obj i = G.obj i

Tactic:
fin_cases i

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.obj ((fun i ↦ i) ⟨0, ⋯⟩) = G.obj ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.obj ((fun i ↦ i) ⟨1, ⋯⟩) = G.obj ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯

Tactic:
fin_cases i

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨0, ⋯⟩) = eqToHom ⋯

case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun i ↦ i) ⟨1, ⋯⟩) = eqToHom ⋯
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' (eqToIso h).hom 0 ⋯ = (eqToIso h₀).hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
by
      rw [w]
      dsimp [app']
      rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
i : Fin (2 + 1)
⊢ IsIso (f.app i)

Tactic:
fin_cases i

Goal state after:
case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨1, ⋯⟩))

case «2»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
⊢ IsIso (f.app ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₂ : C
g' : x₁ ⟶ y₂
g : x₀ ⟶ x₁
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_246 _proof_247)
⊢ mk₂ f f' = mk₂ g g'

Tactic:
obtain rfl : x₂ = y₂ := congr_arg Arrow.rightFunc.obj h₁₂

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_246 _proof_247)
⊢ mk₂ f f' = mk₂ g g'
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.IsRadical ↔ IsReduced (R ⧸ I)

Tactic:
by
  conv_lhs => rw [← @Ideal.mk_ker R _ I]
  exact RingHom.ker_isRadical_iff_reduced_of_surjective Quotient.mk_surjective

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

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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ Ideal.map (algebraMap R S) I = ⊤

Tactic:
apply Ideal.eq_top_of_isUnit_mem

Goal state after:
case hx
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ ?x ∈ Ideal.map (algebraMap R S) I

case h
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ?x

case x
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ S
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn)) = (Ideal.Quotient.mk I) ((algebraMap R S) r * mk' S 1 ⟨m, hm⟩)

Tactic:
simp only [mul_eq_mul_left_iff, map_mul]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) rn) = (Ideal.Quotient.mk I) (mk' S 1 ⟨m, hm⟩) ∨
    (Ideal.Quotient.mk I) ((algebraMap R S) r) = 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : T
⊢ ∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1

Tactic:
by
    obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj N y
    refine ⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩
    simpa [← IsScalarTower.algebraMap_apply] using! e

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * x = 0

Tactic:
← (map_units S s).mul_left_inj,

Goal state after:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * x * (algebraMap R S) ↑s = 0 * (algebraMap R S) ↑s
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : M ⊗[R] N
hx : x ∈ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range
⊢ x ∈ (map m.mkQ n.mkQ).ker

Tactic:
Submodule.mem_sup

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : M ⊗[R] N
hx : ∃ y ∈ (map m.subtype LinearMap.id).range, ∃ z ∈ (map LinearMap.id n.subtype).range, y + z = x
⊢ x ∈ (map m.mkQ n.mkQ).ker
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
h : IsLocalRing S
⊢ (algebraMap R S) x ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
by
    simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using!
      isUnit_to_map_iff S I x

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

Goal state before:
pp: case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = R ∙ x
x_mem : x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem

Goal state after:
case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = R ∙ (algebraMap R S) x
x_mem : (algebraMap R S) x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I