harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_right_of_span_eq (x : V) {y z : V} (h : (ℝ ∙ y) = ℝ ∙ z) :
    (2 : ℤ) • o.oangle x y = (2 : ℤ) • o.oangle x z

Proof state:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝˣ
⊢ 2 • o.oangle x y = 2 • o.oangle x (r • y)

Tactic:
exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : Submodule.span ℝ {y} = Submodule.span ℝ {z}
⊢ 2 • o.oangle x y = 2 • o.oangle x z

Tactic:
rw [Submodule.span_singleton_eq_span_singleton] at h

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : ∃ z_1, z_1 • y = z
⊢ 2 • o.oangle x y = 2 • o.oangle x z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : ∃ z_1, z_1 • y = z
⊢ 2 • o.oangle x y = 2 • o.oangle x z

Tactic:
rcases h with ⟨r, rfl⟩

Result:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝˣ
⊢ 2 • o.oangle x y = 2 • o.oangle x (r • y)
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem tsum_op [T2Space α] :
    ∑' x, op (f x) = op (∑' x, f x)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
h : ¬Summable f
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

Tactic:
have ho := summable_op.not.mpr h

Result:
case neg
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
h : ¬Summable f
ho : ¬Summable fun a => op (f a)
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
h : ¬Summable f
ho : ¬Summable fun a => op (f a)
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

Tactic:
rw [tsum_eq_zero_of_not_summable h, tsum_eq_zero_of_not_summable ho, op_zero]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

Tactic:
by_cases h : Summable f

Result:
case pos
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
h : Summable f
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

case neg
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
h : ¬Summable f
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : T2Space α
h : Summable f
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)

Tactic:
exact h.hasSum.op.tsum_eq

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem of_quotient_center_nilpotent (h : IsNilpotent (G ⧸ center G)) : IsNilpotent G

Proof state:
G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
⊢ IsNilpotent G

Tactic:
obtain ⟨n, hn⟩ := h.nilpotent

Result:
case intro
G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ IsNilpotent G

Proof state:
case intro
G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ IsNilpotent G

Tactic:
use n.succ

Result:
case h
G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ upperCentralSeries G n.succ = ⊤

Proof state:
case h
G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ upperCentralSeries G n.succ = ⊤

Tactic:
simp [← comap_upperCentralSeries_quotient_center, hn]

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem normal_exists_closure_subset [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t)
    (hst : s ⊆ t) : ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s tᶜ
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

Tactic:
rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
  ⟨s', t', hs', ht', hss', htt', hs't'⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ

Tactic:
exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

Tactic:
refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
  (compl_subset_comm.1 htt')⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

Tactic:
have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s tᶜ
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
-- Mathlib/Topology/Category/LightProfinite/AsLimit.lean
lemma lightToProfinite_map_proj_eq (n : ℕ) : lightToProfinite.map (S.proj n) =
    (lightToProfinite.obj S).asLimitCone.π.app _

Proof state:
S : LightProfinite
n : ℕ
⊢ S.proj n =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
let c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone

Result:
S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
⊢ S.proj n =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Proof state:
S : LightProfinite
n : ℕ
⊢ lightToProfinite.map (S.proj n) =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
simp only [Functor.comp_obj, toCompHausLike_map, coe_of]

Result:
S : LightProfinite
n : ℕ
⊢ S.proj n =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Proof state:
S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
hc : IsLimit c := S.toLightDiagram.isLimit
⊢ S.proj n =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
exact liftedLimitMapsToOriginal_inv_map_π hc _

Result:
no goals

Proof state:
S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
⊢ S.proj n =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
let hc : IsLimit c := S.toLightDiagram.isLimit

Result:
S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
hc : IsLimit c := S.toLightDiagram.isLimit
⊢ S.proj n =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.mul_const (hc : HasFDerivAt c c' x) (d : 𝔸') :
    HasFDerivAt (fun y => c y * d) (d • c') x

Proof state:
case h.e'_12.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ d • c' = c'.smulRight d

Tactic:
ext z

Result:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
z : E
⊢ (d • c') z = (c'.smulRight d) z

Proof state:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
z : E
⊢ (d • c') z = (c'.smulRight d) z

Tactic:
apply mul_comm

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HasFDerivAt (fun y => c y * d) (d • c') x

Tactic:
convert hc.mul_const' d

Result:
case h.e'_12.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ d • c' = c'.smulRight d
-- Mathlib/Topology/IndicatorConstPointwise.lean
lemma tendsto_indicator_const_iff_forall_eventually'
    (b : β) (nhd_b : {0}ᶜ ∈ 𝓝 b) (nhd_o : {b}ᶜ ∈ 𝓝 0) :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
      ↔ ∀ x, ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A)

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x))) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
apply forall_congr'

Result:
case h
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ ∀ (a : α),
    Tendsto (fun i => (As i).indicator (fun x => b) a) L (𝓝 (A.indicator (fun x => b) a)) ↔
      ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
simp_rw [tendsto_pi_nhds]

Result:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x))) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Proof state:
case h
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
⊢ ∀ (a : α),
    Tendsto (fun i => (As i).indicator (fun x => b) a) L (𝓝 (A.indicator (fun x => b) a)) ↔
      ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A

Tactic:
exact tendsto_indicator_const_apply_iff_eventually' L b nhd_b nhd_o

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma lt_or_le_of_codirected [SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α} (h₁ : r ≤ v₁)
    (h₂ : r ≤ v₂) : v₁ < v₂ ∨ v₂ ≤ v₁

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
rw [Classical.or_iff_not_imp_right]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ ¬v₂ ≤ v₁ → v₁ < v₂

Proof state:
case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
contradiction

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

Tactic:
apply lt_of_le_of_ne h (ne_of_not_le nh).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ ¬v₂ ≤ v₁ → v₁ < v₂

Tactic:
intro nh

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
⊢ v₁ < v₂

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
rcases le_total_of_codirected h₁ h₂ with h | h

Result:
case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem pullbackSymmetry_hom_of_mono_eq : (pullbackSymmetry f f).hom = 𝟙 _

Proof state:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f

Tactic:
simp [fst_eq_snd_of_mono_eq]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom = 𝟙 (pullback f f)

Tactic:
ext

Result:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f

Proof state:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f

Tactic:
simp [fst_eq_snd_of_mono_eq]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
lemma dvd_C_mul_X_sub_one_pow_add_one {p : ℕ} (hpri : p.Prime)
    (hp : p ≠ 2) (a r : R) (h₁ : r ∣ a ^ p) (h₂ : r ∣ p * a) : C r ∣ (C a * X - 1) ^ p + 1

Proof state:
case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X + -1) ^ p - (-1) ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1

Tactic:
rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X - 1) ^ p + 1

Tactic:
have := hpri.dvd_add_pow_sub_pow_of_dvd (C a * X) (-1) (r := C r) ?_ ?_

Result:
case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X + -1) ^ p - (-1) ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1

case refine_1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X) ^ p

case refine_2
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ ↑p * (C a * X)

Proof state:
case refine_2
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ ↑p * (C a * X)

Tactic:
simp only [map_mul, map_natCast, ← mul_assoc, dvd_mul_right, (_root_.map_dvd C h₂).trans]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ (C a * X) ^ p

Tactic:
simp only [mul_pow, ← map_pow, dvd_mul_right, (_root_.map_dvd C h₁).trans]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_lt_one_iff {x : ℝ} : exp x < 1 ↔ x < 0

Proof state:
x : ℝ
⊢ rexp x < 1 ↔ x < 0

Tactic:
rw [← exp_zero, exp_lt_exp]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem agree_iff_agree' {n : ℕ} (x y : M F) :
    Agree (x.approx n) (y.approx <| n + 1) ↔ Agree' n x y

Proof state:
case mpr.succ.step.f.f.refl.refl
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j => (x' j).approx n✝) (CofixA.intro a fun j => (y' j).approx (n✝ + 1))

Tactic:
constructor

Result:
case mpr.succ.step.f.f.refl.refl.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
⊢ ∀ (i : F.B a), Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))

Proof state:
case mpr.succ.step.f.f.refl
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
⊢ Agree (CofixA.intro a fun j => (x' j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Tactic:
replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›

Result:
case mpr.succ.step.f.f.refl
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
h_a_2 : ⟨y_a, y_f⟩ = ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j => (x' j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))
-- Mathlib/Topology/PartialHomeomorph.lean
theorem Set.EqOn.restr_eqOn_source {e e' : PartialHomeomorph X Y}
    (h : EqOn e e' (e.source ∩ e'.source)) : e.restr e'.source ≈ e'.restr e.source

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.restr e'.source ≈ e'.restr e.source

Tactic:
constructor

Result:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (e.restr e'.source).source = (e'.restr e.source).source

case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source)) (↑(e'.restr e.source)) (e.restr e'.source).source

Proof state:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source)) (↑(e'.restr e.source)) (e.source ∩ e'.source)

Tactic:
refine (EqOn.trans ?_ h).trans ?_ <;> simp only [mfld_simps, eqOn_refl]

Result:
no goals

Proof state:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source)) (↑(e'.restr e.source)) (e.restr e'.source).source

Tactic:
rw [e.restr_source' _ e'.open_source]

Result:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source)) (↑(e'.restr e.source)) (e.source ∩ e'.source)

Proof state:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (e.restr e'.source).source = e'.source ∩ e.source

Tactic:
rw [e.restr_source' _ e'.open_source]

Result:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source

Proof state:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source

Tactic:
exact Set.inter_comm _ _

Result:
no goals

Proof state:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (e.restr e'.source).source = (e'.restr e.source).source

Tactic:
rw [e'.restr_source' _ e.open_source]

Result:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : PartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (e.restr e'.source).source = e'.source ∩ e.source
-- Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
theorem zero : IsTopologicallyNilpotent (0 : R) :=
  tendsto_atTop_of_eventually_const (i₀ := 1)
    (fun _ hi => by rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)])

Proof state:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
x✝ : ℕ
hi : x✝ ≥ 1
⊢ 0 ^ x✝ = 0

Tactic:
rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)]

Result:
no goals