harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem Sum.mem_uniformity_iff_glueDist (hε : 0 < ε) (s : Set ((X ⊕ Y) × (X ⊕ Y))) :
    s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ > 0, ∀ a b, glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) ↔
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Tactic:
constructor

Result:
case mp
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) →
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
    (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

Proof state:
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
⊢ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Tactic:
refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩

Result:
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
⊢ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δX ⊓ δY ⊓ ε → (a, b) ∈ s

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Tactic:
simp only [Sum.uniformity, Filter.mem_sup, Filter.mem_map, mem_uniformity_dist, mem_preimage]

Result:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) ↔
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic_injective [CharZero R] : Function.Injective fun n => cyclotomic n R

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : (cyclotomic m ℂ).IsRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
hmzero : NeZero m
⊢ n = m

Tactic:
rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot

Result:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) m
hmzero : NeZero m
⊢ n = m
-- Mathlib/CategoryTheory/Comma/Basic.lean
@[simp]
lemma inv_right [IsIso e] : (inv e).right = inv e.right

Proof state:
case hom_inv_id
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ e.right ≫ (inv e).right = 𝟙 X.right

Tactic:
rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Result:
no goals

Proof state:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (inv e).right = inv e.right

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ e.right ≫ (inv e).right = 𝟙 X.right
-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem continuousOn_norm_circleTransformBoundingFunction {R r : ℝ} (hr : r < R) (z : ℂ) :
    ContinuousOn ((‖·‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)

Proof state:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)

Tactic:
apply_rules [ContinuousOn.smul, continuousOn_const]

Result:
case hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => deriv (circleMap z R) x.2) (closedBall z r ×ˢ univ)

case hg.hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => ((circleMap z R x.2 - x.1) ^ 2)⁻¹) (closedBall z r ×ˢ univ)

Proof state:
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
⊢ ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)

Tactic:
exact this.norm

Result:
no goals

Proof state:
case hg.hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => ((circleMap z R x.2 - x.1) ^ 2)⁻¹) (closedBall z r ×ˢ univ)

Tactic:
simpa only [inv_pow] using continuousOn_prod_circle_transform_function hr

Result:
no goals

Proof state:
case hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap 0 R x.2 * I) (closedBall z r ×ˢ univ)

Tactic:
apply_rules [ContinuousOn.mul, (continuous_circleMap 0 R).comp_continuousOn continuousOn_snd,
  continuousOn_const]

Result:
no goals

Proof state:
case hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => deriv (circleMap z R) x.2) (closedBall z r ×ˢ univ)

Tactic:
simp only [deriv_circleMap]

Result:
case hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap 0 R x.2 * I) (closedBall z r ×ˢ univ)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem negAt_symm :
    (negAt s).symm = negAt s

Proof state:
case h.h.snd.h
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w

Tactic:
rfl

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

Tactic:
simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prod_symm,
  ContinuousLinearEquiv.prod_apply, piCongrRight_symm_apply, if_pos hw, symm_neg, neg_apply]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
⊢ (negAt s).symm = negAt s

Tactic:
ext x w

Result:
case h.h.fst.h
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

case h.h.snd.h
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w

Proof state:
case h.h.fst.h
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

Tactic:
by_cases hw : w ∈ s

Result:
case pos
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

Proof state:
case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

Tactic:
simp_rw [negAt_apply_isReal_and_not_mem _ hw, negAt, prod_symm,
  ContinuousLinearEquiv.prod_apply, piCongrRight_symm_apply, if_neg hw, refl_symm, refl_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/Banach.lean
lemma bijective_iff_dense_range_and_antilipschitz (f : E →SL[σ] F) :
    Bijective f ↔ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c f

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ ∃ c, AntilipschitzWith c ⇑f

Tactic:
refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩ <;>
simp only [LinearMap.range_eq_top, LinearMapClass.ker_eq_bot, h.1, h.2]

Result:
no goals

Proof state:
case surj
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f

Tactic:
case surj => rwa [← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f

Tactic:
rwa [← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem OrderIso.strictConcaveOn_symm (f : α ≃o β) (hf : StrictConvexOn 𝕜 univ f) :
    StrictConcaveOn 𝕜 univ f.symm

Proof state:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • x' + b • y' < f.symm (a • f x' + b • f y')

Tactic:
rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]

Result:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ f (a • x' + b • y') < a • f x' + b • f y'
-- Mathlib/Data/Set/Basic.lean
lemma inl_compl_union_inr_compl {α β : Type*} {s : Set α} {t : Set β} :
    Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ

Tactic:
rw [compl_union]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s)ᶜ ∩ (Sum.inr '' t)ᶜ

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s)ᶜ ∩ (Sum.inr '' t)ᶜ

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_sub_one {R : Type*} [Ring R] {n : ℕ} (k : ZMod n) :
    (cast (k - 1 : ZMod n) : R) = (if k = 0 then (n : R) else cast k) - 1

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
⊢ (k - 1).cast = (if k = 0 then ↑n else k.cast) - 1

Tactic:
split_ifs with hk

Result:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = ↑n - 1

case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Proof state:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1

Tactic:
rw [Nat.cast_sub, Nat.cast_one]

Result:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k

Proof state:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑↑(k - 1) = ↑↑k - 1

Tactic:
rw [Fin.coe_sub_one, if_neg]

Result:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1

case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0

Proof state:
case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0

Tactic:
exact hk

Result:
no goals

Proof state:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k

Tactic:
rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk

Result:
no goals

Proof state:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Result:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑↑(k - 1) = ↑↑k - 1

Proof state:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1

Tactic:
rw [Int.cast_sub, Int.cast_one]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
cases n

Result:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Proof state:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = ↑n - 1

Tactic:
rw [hk, zero_sub, ZMod.cast_neg_one]

Result:
no goals

Proof state:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
dsimp [ZMod, ZMod.cast]

Result:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_union_Icc' (h₁ : c ≤ b) : Iic b ∪ Icc c d = Iic (max b d)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
simp only [hc, true_and]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x ≤ b
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
simp only [hxb, true_or]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
by_cases hc : c ≤ x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iic b ∪ Icc c d ↔ x ∈ Iic (b ⊔ d)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x ≤ b
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iic b ∪ Icc c d ↔ x ∈ Iic (b ⊔ d)

Tactic:
simp_rw [mem_union, mem_Iic, mem_Icc, le_max_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c ≤ b
x : α
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_le_mul_of_nonneg_left {a b c : Int}
    (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
  if hba : b ≤ a then by
    rw [Int.le_antisymm hba h₁]; apply Int.le_refl
  else if hc0 : c ≤ 0 then by
    simp [Int.le_antisymm hc0 h₂, Int.zero_mul]
  else by
    exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
      (Int.lt_iff_le_not_le.2 ⟨h₁, hba⟩) (Int.lt_iff_le_not_le.2 ⟨h₂, hc0⟩)

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : ¬b ≤ a
hc0 : ¬c ≤ 0
⊢ c * a ≤ c * b

Tactic:
exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
  (Int.lt_iff_le_not_le.2 ⟨h₁, hba⟩) (Int.lt_iff_le_not_le.2 ⟨h₂, hc0⟩)

Result:
no goals

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : b ≤ a
⊢ c * a ≤ c * a

Tactic:
apply Int.le_refl

Result:
no goals

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : b ≤ a
⊢ c * a ≤ c * b

Tactic:
rw [Int.le_antisymm hba h₁]

Result:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : b ≤ a
⊢ c * a ≤ c * a

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
hba : ¬b ≤ a
hc0 : c ≤ 0
⊢ c * a ≤ c * b

Tactic:
simp [Int.le_antisymm hc0 h₂, Int.zero_mul]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem clusterPt_iff_lift'_closure' {F : Filter X} :
    ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot

Proof state:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
h : pure x ≤ F.lift' closure
⊢ (pure x ⊓ F.lift' closure).NeBot

Tactic:
simp [h, pure_neBot]

Result:
no goals

Proof state:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure
h : ∀ (s : Set X), (∃ t₁ ∈ pure x, ∃ t₂ ∈ F.lift' closure, s = t₁ ∩ t₂) → s.Nonempty
⊢ U ∈ pure x

Tactic:
simpa using h ({x} ∩ U) ⟨{x}, by simp, U, hU, rfl⟩

Result:
no goals

Proof state:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
h : (pure x ⊓ F.lift' closure).NeBot
U : Set X
hU : U ∈ F.lift' closure
⊢ U ∈ pure x

Tactic:
simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h

Result:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure
h : ∀ (s : Set X), (∃ t₁ ∈ pure x, ∃ t₂ ∈ F.lift' closure, s = t₁ ∩ t₂) → s.Nonempty
⊢ U ∈ pure x

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure
h : ∀ (s : Set X), (∃ t₁ ∈ pure x, ∃ t₂ ∈ F.lift' closure, s = t₁ ∩ t₂) → s.Nonempty
⊢ {x} ∈ pure x

Tactic:
simp

Result:
no goals

Proof state:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ pure x ≤ F.lift' closure → (pure x ⊓ F.lift' closure).NeBot

Tactic:
intro h

Result:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
h : pure x ≤ F.lift' closure
⊢ (pure x ⊓ F.lift' closure).NeBot

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot

Tactic:
rw [clusterPt_iff_lift'_closure, inf_comm]

Result:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ pure x ≤ F.lift' closure ↔ (pure x ⊓ F.lift' closure).NeBot

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ pure x ≤ F.lift' closure ↔ (pure x ⊓ F.lift' closure).NeBot

Tactic:
constructor

Result:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ pure x ≤ F.lift' closure → (pure x ⊓ F.lift' closure).NeBot

case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ (pure x ⊓ F.lift' closure).NeBot → pure x ≤ F.lift' closure

Proof state:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ (pure x ⊓ F.lift' closure).NeBot → pure x ≤ F.lift' closure

Tactic:
intro h U hU

Result:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
h : (pure x ⊓ F.lift' closure).NeBot
U : Set X
hU : U ∈ F.lift' closure
⊢ U ∈ pure x
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_prod_sInter {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempty) (hT : T.Nonempty) :
    ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_

Result:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : x ∈ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Proof state:
case intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hT : T.Nonempty
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₂, h₂⟩ := hT

Result:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : x ∈ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Tactic:
rw [mem_iInter₂] at hx

Result:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ i ∈ S ×ˢ T, x ∈ i.1 ×ˢ i.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Proof state:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hS : S.Nonempty
hT : T.Nonempty
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₁, h₁⟩ := hS

Result:
case intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hT : T.Nonempty
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ i ∈ S ×ˢ T, x ∈ i.1 ×ˢ i.2
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T

Tactic:
exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_mul_nat (o : Ordinal) : (sup fun n : ℕ => o * n) = o * ω

Proof state:
o : Ordinal.{u_1}
⊢ (sup fun n => o * ↑n) = o * ω

Tactic:
rcases eq_zero_or_pos o with (rfl | ho)

Result:
case inl

⊢ (sup fun n => 0 * ↑n) = 0 * ω

case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o * ↑n) = o * ω

Proof state:
case inl

⊢ (sup fun n => 0 * ↑n) = 0 * ω

Tactic:
rw [zero_mul]

Result:
case inl

⊢ (sup fun n => 0 * ↑n) = 0

Proof state:
case inl

⊢ (sup fun n => 0 * ↑n) = 0

Tactic:
exact sup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal)

Result:
no goals

Proof state:
case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o * ↑n) = o * ω

Tactic:
exact (mul_isNormal ho).apply_omega0

Result:
no goals