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

Goal state before:
pp: case refine_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x ↦ (AddMonoidHom.mul x.1) x.2) (0, 0)

pp: case refine_2
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (⇑(AddMonoidHom.mul x)) 0

pp: case refine_3
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R), ContinuousAt (fun x ↦ (AddMonoidHom.mul x) y) 0

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x ↦ (AddMonoidHom.mul x.1) x.2) (0, 0)

case refine_2
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (⇑(AddMonoidHom.mul x)) 0

case refine_3
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R), ContinuousAt (fun x ↦ (AddMonoidHom.mul x) y) 0
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x

Tactic:
rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ (univ.pi fun i ↦ Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀) := by
    rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
      inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
h✝ : x' w < a w
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
h✝ : a w ≤ x' w
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
h✝ : x' w < a w
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True

case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
h✝ : a w ≤ x' w
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inr.inr.h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ Dense (range fun x ↦ a⁻¹ ^ x)

pp: case inr.inr.ha₀
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ 1 < a⁻¹

Tactic:
<;>

Goal state after:
case inr.inr.h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ Dense (range fun x ↦ a⁻¹ ^ x)

case inr.inr.ha₀
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ 1 < a⁻¹
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = 𝓤 G

Tactic:
@IsLeftUniformGroup.uniformity_eq (G := G) us _ _

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

pp: case h₂
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

Tactic:
<;>

Goal state after:
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

case h₂
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ i ∈ s.1, (Ioi ↑i).OrdConnected

pp: case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ i ∈ s.2, (Iio ↑i).OrdConnected

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ i ∈ s.1, (Ioi ↑i).OrdConnected

case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ i ∈ s.2, (Iio ↑i).OrdConnected
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : PartialEquiv α β), x.EqOnSource x

pp: case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x

pp: case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y z : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource z → x.EqOnSource z

Tactic:
<;>

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : PartialEquiv α β), x.EqOnSource x

case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x

case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y z : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource z → x.EqOnSource z
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm) (↑e) e.symm.source

pp: case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ MapsTo (↑e'.symm) e.symm.source e.source

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm) (↑e) e.symm.source

case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ MapsTo (↑e'.symm) e.symm.source e.source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ (↑(e.prod e').symm x).1 = (↑(e.symm.prod e'.symm) x).1

pp: case h.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ (↑(e.prod e').symm x).2 = (↑(e.symm.prod e'.symm) x).2

pp: case hsymm.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ (↑(e.prod e').symm.symm x).1 = (↑(e.symm.prod e'.symm).symm x).1

pp: case hsymm.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ (↑(e.prod e').symm.symm x).2 = (↑(e.symm.prod e'.symm).symm x).2

pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ x ∈ (e.prod e').symm.source ↔ x ∈ (e.symm.prod e'.symm).source

Tactic:
<;>

Goal state after:
case h.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ (↑(e.prod e').symm x).1 = (↑(e.symm.prod e'.symm) x).1

case h.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ (↑(e.prod e').symm x).2 = (↑(e.symm.prod e'.symm) x).2

case hsymm.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ (↑(e.prod e').symm.symm x).1 = (↑(e.symm.prod e'.symm).symm x).1

case hsymm.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ (↑(e.prod e').symm.symm x).2 = (↑(e.symm.prod e'.symm).symm x).2

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ x ∈ (e.prod e').symm.source ↔ x ∈ (e.symm.prod e'.symm).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.fst
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) (x, y)).1 = (↑(PartialEquiv.refl (α × β)) (x, y)).1

pp: case h.snd
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) (x, y)).2 = (↑(PartialEquiv.refl (α × β)) (x, y)).2

pp: case hsymm.fst
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm (x, y)).1 = (↑(PartialEquiv.refl (α × β)).symm (x, y)).1

pp: case hsymm.snd
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm (x, y)).2 = (↑(PartialEquiv.refl (α × β)).symm (x, y)).2

pp: case hs
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (x, y) ∈ ((PartialEquiv.refl α).prod (PartialEquiv.refl β)).source ↔ (x, y) ∈ (PartialEquiv.refl (α × β)).source

Tactic:
<;>

Goal state after:
case h.fst
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) (x, y)).1 = (↑(PartialEquiv.refl (α × β)) (x, y)).1

case h.snd
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) (x, y)).2 = (↑(PartialEquiv.refl (α × β)) (x, y)).2

case hsymm.fst
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm (x, y)).1 = (↑(PartialEquiv.refl (α × β)).symm (x, y)).1

case hsymm.snd
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm (x, y)).2 = (↑(PartialEquiv.refl (α × β)).symm (x, y)).2

case hs
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (x, y) ∈ ((PartialEquiv.refl α).prod (PartialEquiv.refl β)).source ↔ (x, y) ∈ (PartialEquiv.refl (α × β)).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (↑((e.prod e').trans (f.prod f')) (x, y)).1 = (↑((e.trans f).prod (e'.trans f')) (x, y)).1

pp: case h.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (↑((e.prod e').trans (f.prod f')) (x, y)).2 = (↑((e.trans f).prod (e'.trans f')) (x, y)).2

pp: case hsymm.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ (↑((e.prod e').trans (f.prod f')).symm (x, y)).1 = (↑((e.trans f).prod (e'.trans f')).symm (x, y)).1

pp: case hsymm.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ (↑((e.prod e').trans (f.prod f')).symm (x, y)).2 = (↑((e.trans f).prod (e'.trans f')).symm (x, y)).2

pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source

Tactic:
<;>

Goal state after:
case h.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (↑((e.prod e').trans (f.prod f')) (x, y)).1 = (↑((e.trans f).prod (e'.trans f')) (x, y)).1

case h.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (↑((e.prod e').trans (f.prod f')) (x, y)).2 = (↑((e.trans f).prod (e'.trans f')) (x, y)).2

case hsymm.fst
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ (↑((e.prod e').trans (f.prod f')).symm (x, y)).1 = (↑((e.trans f).prod (e'.trans f')).symm (x, y)).1

case hsymm.snd
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : γ
y : ε
⊢ (↑((e.prod e').trans (f.prod f')).symm (x, y)).2 = (↑((e.trans f).prod (e'.trans f')).symm (x, y)).2

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x, y) ∈ ((e.prod e').trans (f.prod f')).source ↔ (x, y) ∈ ((e.trans f).prod (e'.trans f')).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)) x✝¹ x✝

pp: case hsymm
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).symm x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)).symm x✝¹ x✝

pp: case hs
ι : Type u_5
αi : ι → Type u_6
x✝ : (i : ι) → αi i
⊢ x✝ ∈ (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).source ↔ x✝ ∈ (PartialEquiv.refl ((i : ι) → αi i)).source

Tactic:
<;>

Goal state after:
case h
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)) x✝¹ x✝

case hsymm
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).symm x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)).symm x✝¹ x✝

case hs
ι : Type u_5
αi : ι → Type u_6
x✝ : (i : ι) → αi i
⊢ x✝ ∈ (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).source ↔ x✝ ∈ (PartialEquiv.refl ((i : ι) → αi i)).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case h
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')) x✝¹ x✝ = ↑(PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)) x✝¹ x✝

pp: case hsymm
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝¹ : (i : ι) → γi i
x✝ : ι
⊢ ↑((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')).symm x✝¹ x✝ =
    ↑(PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)).symm x✝¹ x✝

pp: case hs
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝ : (i : ι) → αi i
⊢ x✝ ∈ ((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')).source ↔
    x✝ ∈ (PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)).source

Tactic:
<;>

Goal state after:
case h
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')) x✝¹ x✝ = ↑(PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)) x✝¹ x✝

case hsymm
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝¹ : (i : ι) → γi i
x✝ : ι
⊢ ↑((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')).symm x✝¹ x✝ =
    ↑(PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)).symm x✝¹ x✝

case hs
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝ : (i : ι) → αi i
⊢ x✝ ∈ ((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')).source ↔
    x✝ ∈ (PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)).source
Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderSubobjects
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₁

Tactic:
have := hS.mono_f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderSubobjects
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
this : Mono S.f
⊢ P S.X₁
Module: Mathlib.CategoryTheory.ObjectProperty.Extensions

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u'
inst✝⁶ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : P.IsClosedUnderExtensions
F : D ⥤ C
inst✝³ : HasZeroMorphisms D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
S✝ : ShortComplex D
hS : S✝.ShortExact
h₁ : P.inverseImage F S✝.X₁
h₃ : P.inverseImage F S✝.X₃
⊢ P.inverseImage F S✝.X₂

Tactic:
have := hS.mono_f

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u'
inst✝⁶ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : P.IsClosedUnderExtensions
F : D ⥤ C
inst✝³ : HasZeroMorphisms D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
S✝ : ShortComplex D
hS : S✝.ShortExact
h₁ : P.inverseImage F S✝.X₁
h₃ : P.inverseImage F S✝.X₃
this : Mono S✝.f
⊢ P.inverseImage F S✝.X₂
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
e : A ≃ₗ[R] B
c : CharacterModule B
x✝ : B
⊢ ((dual ↑e.symm ∘ₗ dual ↑e) c) x✝ = (LinearMap.id c) x✝

Tactic:
exact congr(c $(e.right_inv _))

Goal state after:
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:
rw [← nhdsLT_sup_nhdsGE, Filter.EventuallyEq, Filter.eventually_sup]

Goal state after:
𝕜 : 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]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
hy : x ≠ x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

pp: case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
· exact (hy rfl).elim

Goal state after:
case inr.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s