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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim : Tendsto ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 0)
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
rw [tendsto_prod_self_iff] at lim

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'
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 : ι
a : α i
⊢ update f i '' Icc a (f i) = Icc (update f i a) f

Tactic:
simpa using image_update_Icc f i a (f i)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
⊢ (DenseRange fun x ↦ a ^ x) ↔ Surjective fun x ↦ a ^ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩
  wlog! ha₀ : 1 < a generalizing a
  · simp only [← range_eq_univ, DenseRange] at *
    rcases ha₀.eq_or_lt with rfl | hlt
    · simpa only [one_zpow, range_const, dense_iff_closure_eq, closure_singleton] using h
    · have H : range (a⁻¹ ^ · : ℤ → G) = range (a ^ · : ℤ → G) := by
        simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)
      rw [← H]
      apply this <;> simpa only [H, one_lt_inv']
  intro b
  obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) := by
    have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne
  rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne; · simp
  suffices (Ioo (a ^ m) (a ^ (m + 1))).Nonempty by
    rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
    have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
    lia
  rcases hne.lt_or_gt with hlt | hlt
  · refine ⟨b * a * a, hm', ?_⟩
    simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt,
      mul_lt_mul_iff_right] using hlt
  · use b * a
    simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢
    exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]
  exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

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✝, Preorder.topology α] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)

Tactic:
continuous_generateFrom_iff

Goal state after:
α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ (∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝] (f ⁻¹' s)) ↔
    ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x

pp: case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑e.symm x = ↑e'.symm x

Tactic:
· apply h.2
    rw [s]
    exact mem_univ _

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑e.symm x = ↑e'.symm x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIcoDiv hp a =ᶠ[𝓝 x] fun x_1 ↦ toIcoDiv hp a x

Tactic:
by
  rw [← nhdsLT_sup_nhdsGE, Filter.EventuallyEq, Filter.eventually_sup]
  refine ⟨?_, eventuallyEq_toIcoDiv_nhdsGE hp a x⟩
  convert! (eventuallyEq_toIcoDiv_nhdsLT hp a x).eventually using 3
  rwa [← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
hy : n • y = ↑(f x') • p
y' : 𝕜
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'

Tactic:
← hy',

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
x x' : ↑{x | n • x = 0}
eq : f x = f x'
y : 𝕜
hyx : ↑y = ↑x
y' : 𝕜
hy : n • y = n • y'
hyx' : ↑y' = ↑x'
hy' : n • y' = ↑(f x') • p
⊢ ↑x = ↑x'
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift (AddEquiv.ulift.symm (χ ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)

Tactic:
AddEquiv.apply_symm_apply

Goal state after:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ χ ((Quot.ι F j) x) = χ ((Quot.ι F j) x)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((r • f).sum fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
rw [Finsupp.sum_smul_index]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun i a ↦ sum g fun g' t ↦ single (i ≫ g') (r * a * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), (sum g fun g' t ↦ single (i ≫ g') (0 * t)) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ((r • g).sum fun g' t ↦ single (h ≫ g') (s * t)) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

Tactic:
rw [Finsupp.sum_smul_index]

Goal state after:
case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ (sum g fun i a ↦ single (h ≫ i) (s * (r * a))) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), single (h ≫ i) (s * 0) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum (r • f) fun f' r ↦ r • F.map f') = r • sum f fun f' r ↦ r • F.map f'

Tactic:
rw [Finsupp.sum_smul_index]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum f fun i a ↦ (r * a) • F.map i) = r • sum f fun f' r ↦ r • F.map f'

R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ ∀ (i : X ⟶ Y), 0 • F.map i = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
⊢ x = y

Tactic:
apply ConcreteCategory.injective_of_mono_of_preservesPullback (PreservesProduct.iso F f).hom

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
⊢ (hom (PreservesProduct.iso F f).hom) x = (hom (PreservesProduct.iso F f).hom) y
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst✝¹ : HasPullback f₁ f₂
inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)
x₁ : ToType X₁
x₂ : ToType X₂
h : (hom f₁) (x₁, x₂).1 = (hom f₂) (x₁, x₂).2
⊢ ∃ x₁_1 x₂_1,
    ∃ (h_1 : (hom f₁) x₁_1 = (hom f₂) x₂_1), (pullbackEquiv f₁ f₂).symm ⟨(x₁, x₂), h⟩ = pullbackMk f₁ f₂ x₁_1 x₂_1 h_1

Tactic:
exact ⟨x₁, x₂, h, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ x = y

Tactic:
apply Concrete.widePullback_ext _ _ _ _ h
  inhabit ι
  simp only [← π_arrow f default, ConcreteCategory.comp_apply, h]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: 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
⊢ { l //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }

Tactic:
refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩

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.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ (beckCoalgebraFork X).pt.a

case refine_2
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
⊢ { f := s.ι.f ≫ T.ε.app X.A, h := ?refine_1 } ≫ (beckCoalgebraFork X).ι = s.ι

case refine_3
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
⊢ ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt},
    m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ?refine_1 }
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)

Tactic:
by
  obtain ⟨_ | _, hi⟩ := i <;> simp

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

Goal state before:
pp: case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯ ≫ homOfLE ⋯)

Tactic:
homOfLE_comp

Goal state after:
case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯ ≫ homOfLE ⋯)

Tactic:
homOfLE_comp

Goal state after:
case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯)
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
⊢ (a + b) • s ⊆ a • s + b • s

Tactic:
rintro _ ⟨x, hx, rfl⟩
  simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊤ = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ⊤ ≤ localized₀ p f ⊤
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ IsLocalizedModule.mk' f a s ∈ I • localized₀ p f M'

Tactic:
refine Submodule.smul_induction_on ha ?_ ?_

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ ∀ r ∈ I, ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

case a.refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ ∀ (x y : M),
    IsLocalizedModule.mk' f x s ∈ I • localized₀ p f M' →
      IsLocalizedModule.mk' f y s ∈ I • localized₀ p f M' → IsLocalizedModule.mk' f (x + y) s ∈ I • localized₀ p f M'
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.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
Ideal.quotientMap_mk,

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) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
⊢ Function.Injective ⇑f

Tactic:
have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this✝ : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
this : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
⊢ Function.Injective ⇑f
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
⊢ Function.Surjective ⇑f

Tactic:
have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this✝ : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
this : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
⊢ Function.Surjective ⇑f
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ S.mkQ (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • S.mkQ (m ⊗ₜ[R] n)

Tactic:
Submodule.mkQ_apply,

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ Submodule.Quotient.mk (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • S.mkQ (m ⊗ₜ[R] n)