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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))).NeBot

Tactic:
apply comap_neBot

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ ∀ t ∈ 𝓝 (x₀, y₀), ∃ a, Prod.map (⇑e) (⇑f) a ∈ t
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : x ∈ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
h'x : ¬IsTop x
⊢ x ∈ t ∪ {x | IsTop x}

Tactic:
· simpa [-sep_and, t, h'x]

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s, (⨅ i, ⨅ (_ : s = Ioi i), ⨅ (_ : a ∈ s), 𝓟 s) ⊓ ⨅ i, ⨅ (_ : s = Iio i), ⨅ (_ : a ∈ s), 𝓟 s =
    (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
iInf_inf_eq,

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ x, ⨅ i, ⨅ (_ : x = Ioi i), ⨅ (_ : a ∈ x), 𝓟 x) ⊓ ⨅ x, ⨅ i, ⨅ (_ : x = Iio i), ⨅ (_ : a ∈ x), 𝓟 x =
    (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderTopology (α i)
f : (i : ι) → α i
i : ι
this : Tendsto (fun g ↦ g i) (𝓝 f) (𝓝 (f i))
⊢ ∀ᶠ (x : ((i : ι) → α i) × ((i : ι) → α i)) in 𝓝 f ×ˢ 𝓝 f,
    (image (eval i) ∘ fun p ↦ Icc p.1 p.2) x ⊆ Icc (((fun g ↦ g i) ∘ Prod.fst) x) (((fun g ↦ g i) ∘ Prod.snd) x)

Tactic:
filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∃ x, ¬f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
· rcases h with ⟨x, hx⟩
      rcases H₂ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)

Goal state after:
case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
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 : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, x_1 ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
apply Ioc_mem_nhdsLE_of_mem

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (c + c').toAddMonoidHom ⋯) x = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) x

Tactic:
by refine x.induction_on ?_ ?_ ?_ <;> aesop

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ liftIoc p a f ↑↑((equivIco p a) x) = liftIco p a f ↑↑((equivIco p a) x)

Tactic:
liftIco_coe_apply (equivIco p a x).coe_prop

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ liftIoc p a f ↑↑((equivIco p a) x) = f ↑((equivIco p a) x)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ addOrderOf ↑(p / ↑n) = n

Tactic:
addOrderOf_eq_iff h

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ m < n, 0 < m → m • ↑(p / ↑n) ≠ 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = n.totient

Tactic:
rw [← coe_ofPred, Nat.card_congr (setAddOrderOfEquiv p hn),
      n.totient_eq_card_lt_and_coprime]
    simp only [Nat.gcd_comm]

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

Goal state before:
pp: J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Function.Bijective ⇑(Quot.desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c))

Tactic:
← Function.Bijective.of_comp_iff _
          (quotQuotUliftAddEquiv F).bijective,

Goal state after:
J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Function.Bijective (⇑(Quot.desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ∘ ⇑(quotQuotUliftAddEquiv F))
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 0
i : ℕ
hi : i + 2 ≤ 0
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
by simp at hi

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 0
i : ℕ
hi : i + 2 ≤ 0
⊢ (S.sc ⋯ i hi).Exact

Tactic:
by simp at hi

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.IsComplex →
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0 →
    S.IsComplex

Tactic:
· intro h
    exact h.zero 0 (by lia)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0 →
    S.IsComplex
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] <;> simp [mul_left_comm]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))

Tactic:
by
  rw [← AddCommGrpCat.mono_iff_injective]
  constructor
  · intro
    infer_instance
  · apply Functor.mono_of_mono_map

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.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
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃ ≫ D.v₁₂.τ₂)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom D.L₂.f) x₁

Tactic:
rw [ConcreteCategory.comp_apply, eq₁]

Goal state after:
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
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.v₁₂.τ₂) x₂ = (ConcreteCategory.hom D.L₂.f) x₁
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
⊢ { l //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }

Tactic:
have h₂ : s.pt.a ≫ (T : C ⥤ C).map s.ι.f = s.ι.f ≫ T.δ.app X.A := s.ι.h

Goal state after:
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 }
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 0
f : F.obj' 0 homMk₀._proof_1 ⟶ G.obj' 0 homMk₀._proof_1
i : ℕ
hi : i < 0
⊢ (F.map' i (i + 1) ⋯ hi ≫
      match ⟨i + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => f) =
    (match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => f) ≫
      G.map' i (i + 1) ⋯ hi

Tactic:
by simp at hi

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 0
h : F.obj' 0 homMk₀._proof_1 = G.obj 0
i : ℕ
hi : i < 0
⊢ F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
by simp at hi

Goal state after:
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 ⋯
⊢ F = G

Tactic:
have : ∀ i, F.obj i = G.obj i := by
    intro ⟨i, hi⟩
    rcases i with - | i
    · exact h₀
    · exact Functor.congr_obj h ⟨i, by valid⟩

Goal state after:
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 = G
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F

Tactic:
let _ :
        F.IsCosplitPair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) :=
        ComonadicityInternal.main_pair_F_cosplit _ ((comparison adj).obj Y)

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
x✝ : F.IsCosplitPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) :=
  main_pair_F_cosplit adj ((comparison adj).obj Y)
⊢ ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : HasEqualizerOfIsCosplitPair F
inst✝ : PreservesLimitOfIsCosplitPair F
A✝ B✝ : C
f g : A✝ ⟶ B✝
x✝ : F.IsCosplitPair f g
⊢ ReflectsLimit (parallelPair f g) F

Tactic:
have := HasEqualizerOfIsCosplitPair.out F f g
    apply reflectsLimit_of_reflectsIsomorphisms

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective
    (⇑(cancelBaseChange R S S M P) ∘ ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype)))

Tactic:
EquivLike.comp_injective

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
obj : Fin (0 + 1) → C
mapSucc : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ
i : ℕ
hi : i < 0
⊢ mapSucc ⟨i, hi⟩ =
    ((fun x ↦
            match x with
            | 0 => Iso.refl ((mk₀ (obj 0)).obj 0))
          ⟨i, ⋯⟩).inv ≫
      (mk₀ (obj 0)).map' i (i + 1) ⋯ hi ≫
        ((fun x ↦
              match x with
              | 0 => Iso.refl ((mk₀ (obj 0)).obj 0))
            ⟨i + 1, ⋯⟩).hom

Tactic:
by simp at hi

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

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ p ↔ (algebraMap A B) x ∈ P

Tactic:
rw [P.over_def p]
  rfl

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ = ⊥

Tactic:
eq_bot_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ ≤ ⊥
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ nilradical R = ⊥ ↔ IsReduced R

Tactic:
eq_bot_iff,

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
⊢ nilradical R ≤ ⊥ ↔ IsReduced R
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ I ^ (2 * n.succ) = ⊥

Tactic:
eq_bot_iff,

Goal state after:
case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ I ^ (2 * n.succ) ≤ ⊥
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
x : ↥p
⊢ IsUnit ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x)

Tactic:
refine (Module.End.isUnit_iff _).mpr ⟨fun m n e ↦ ?_, fun m ↦ ⟨(IsLocalization.mk' S 1 x) • m,
      by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
x : ↥p
m n : N ⧸ localized' S p f M'
e :
  ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x) m =
    ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x) n
⊢ m = n
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.refine_1
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
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.under R J

Tactic:
rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

Tactic:
toFunLinear_tmul_apply,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ((toFunBilinear R A) 1) 1 = 1
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
⊢ (EssFiniteType.subalgebra R S).FG

Tactic:
EssFiniteType.subalgebra

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
⊢ (adjoin R ↑(EssFiniteType.finset R S)).FG