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

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (unitsEquivPos R).toFun

Tactic:
by
    rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
    exact Continuous.subtype_val (p := (0 ≤ ·)) Units.continuous_val

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

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
use b * a

Goal state after:
case h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
⊢ b * a ∈ Ioo (a ^ m) (a ^ (m + 1))
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)

Tactic:
lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
  rw [← neg_pos, ← h, Nat.cast_pos] at hn
  simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'

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

Goal state before:
pp: case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
rintro ⟨u, au, as⟩

Goal state after:
case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioo a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioc a u ⊆ s
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioc a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
rintro ⟨u, au, as⟩

Goal state after:
case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioc a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioo a u ⊆ s
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioc a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
· rintro ⟨u, au, as⟩
    exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.divRight a) x > 1), 𝓟 {a_1 | ((Equiv.divRight a) x)⁻¹ < a / a_1} = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)

Tactic:
simp [Iio]

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

Goal state before:
pp: case refine_1.negSucc
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x ↦ c * x ^ Int.negSucc n) atTop (𝓝 d)
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0

Tactic:
| negSucc n =>

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'✝ e' : PartialEquiv β γ
h : e.target = e'.source
y : γ
hy : y ∈ e'.target
⊢ (↑e' ∘ ↑e) ((↑e.symm ∘ ↑e'.symm) y) = y

Tactic:
by simp [hy, h]

Goal state after:
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
a : A
x : ℤ
⊢ x ∈ (LinearMap.toSpanSingleton ℤ A a).ker ↔ x ∈ Ideal.span {↑(addOrderOf a)}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
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
a : A
x : ℤ
⊢ x ∈ (LinearMap.toSpanSingleton ℤ A a).ker ↔ ↑(addOrderOf a) ∣ x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
x : β
hx : x ∈ s
y : β
hy : y ∈ s
⊢ x < y → f x < f y

Tactic:
hxy

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x < y
⊢ f x < f y
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
s : Set α
s_count : s.Countable
hs : Dense s
⊢ atTop.IsCountablyGenerated

Tactic:
have : atTop = generate (Ici '' s) := by
      refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
      simp only [eq_empty_iff_forall_notMem, IsTop, mem_ofPred_eq, not_forall, not_le] at h
      obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
      exact (hx hy).not_gt hxy

Goal state after:
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ atTop.IsCountablyGenerated
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), OrderTopology (X i)
a b x : (i : ι) → X i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioc a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), OrderTopology (X i)
a b x : (i : ι) → X i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioc (a i) (b i) ∈ 𝓝 (x i)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ ↟(Finsupp.lapply PUnit.unit) ≫ ↟(Finsupp.lsingle PUnit.unit) = 𝟙 ((free R).obj (𝟙_ (Type u)))

Tactic:
ext ⟨⟩
    dsimp [freeMk]
    erw [Finsupp.lapply_apply, Finsupp.lsingle_apply]
    rw [Finsupp.single_eq_same]

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
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δ₀.Exact

Tactic:
by
  rw [exact_iff_δ₀] at hS
  exact hS.2

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S.v₀₁.τ₁ = y₁ := ⟨_, S.exact_C₁_up.lift_f y₁ hy₁'⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
x₁ : A₁ ⟶ S.L₀.X₁
hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
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 w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ IsEmpty (ToType X)

Tactic:
rw [← Types.initial_iff_empty]

Goal state after:
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✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ Nonempty (IsInitial (ToType X))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : zero.Hom Y✝
⊢ (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)

Tactic:
cases g

Goal state after:
case left.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)

case left.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case right
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : zero.Hom Y✝
⊢ (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)

Tactic:
cases g

Goal state after:
case right.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)

case right.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case reflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)

Tactic:
cases g

Goal state after:
case reflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)

case reflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)

case reflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)

case reflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)

case reflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case leftCompReflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)

Tactic:
cases g

Goal state after:
case leftCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)

case leftCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)

case leftCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h = Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)

case leftCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)

case leftCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case rightCompReflexion
Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : one.Hom Y✝
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)

Tactic:
cases g

Goal state after:
case rightCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)

case rightCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)

case rightCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)

case rightCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)

case rightCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case id
W✝ Y✝ Z✝ : WalkingReflexivePair
h : Y✝.Hom Z✝
g : W✝.Hom Y✝
⊢ ((Hom.id W✝).comp g).comp h = (Hom.id W✝).comp (g.comp h)

Tactic:
cases g

Goal state after:
case id.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)

case id.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)

case id.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)

case id.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)

case id.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)

case id.id
W✝ Z✝ : WalkingReflexivePair
h : W✝.Hom Z✝
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp h = (Hom.id W✝).comp ((Hom.id W✝).comp h)
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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ (G ⋙ F).map f.f) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)

Tactic:
rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]

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

Goal state before:
pp: case left
Z✝ : WalkingParallelPair
g : one ⟶ Z✝
⊢ (match Z✝, zero, WalkingParallelPairHom.left ≫ g with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match one, zero, WalkingParallelPairHom.left with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match Z✝, one, g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
cases g

Goal state after:
case left.id
⊢ (match one, zero, WalkingParallelPairHom.left ≫ WalkingParallelPairHom.id one with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match one, zero, WalkingParallelPairHom.left with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, one, WalkingParallelPairHom.id one with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case right
Z✝ : WalkingParallelPair
g : one ⟶ Z✝
⊢ (match Z✝, zero, WalkingParallelPairHom.right ≫ g with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match one, zero, WalkingParallelPairHom.right with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match Z✝, one, g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)

Tactic:
cases g

Goal state after:
case right.id
⊢ (match one, zero, WalkingParallelPairHom.right ≫ WalkingParallelPairHom.id one with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match one, zero, WalkingParallelPairHom.right with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match one, one, WalkingParallelPairHom.id one with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ c.ι.app j ≫ (liftedCocone D c t).pt.a ≫ T.map (t.desc (T.forget.mapCocone s)) =
    c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a

Tactic:
dsimp
          rw [← Category.assoc, ← Category.assoc, t.fac, newCocone_ι_app, t.fac,
            Functor.mapCocone_ι_app, Category.assoc, ← Functor.map_comp, t.fac]
          apply (s.ι.app j).h

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
⊢ x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
hxy

Goal state after:
case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I.radical
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
⊢ ¬Disjoint ↑M ↑I ↔ ∃ m ∈ M, m * 1 ∈ I

Tactic:
simp [Set.disjoint_left]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ IsUnit ((mk (I ^ n)) x) ↔ x ∉ I

Tactic:
rw [isUnit_mk_pow_iff_isUnit_mk I hn, isUnit_iff_ne_zero]

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ (mk I) x ≠ 0 ↔ x ∉ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp.refine_2
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 : J.IsPrime
x y : R
⊢ x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J

Tactic:
hxy

Goal state after:
case mp.refine_2
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 : J.IsPrime
x y : R
hxy : x * y ∈ Ideal.under R J
⊢ x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.refine_2
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)
x y : S
⊢ x * y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
hxy

Goal state after:
case mpr.refine_2
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)
x y : S
hxy : x * y ∈ J
⊢ x ∈ J ∨ y ∈ J
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
x : A[X]
⊢ (toFunAlgHom R A) (invFun R A x) = x

Tactic:
by
  refine Polynomial.induction_on' x ?_ ?_
  · intro p q hp hq
    simp only [invFun_add, map_add, hp, hq]
  · intro n a
    rw [invFun_monomial, Algebra.TensorProduct.tmul_pow,
        one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
        X_pow_eq_monomial, sum_monomial_index] <;>
      simp

Goal state after: