harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/Basic.lean
theorem StrictMono.induced_topology_eq_preorder {α β : Type*} [LinearOrder α]
    [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β}
    (hf : StrictMono f) (hc : OrdConnected (range f)) : t.induced f = Preorder.topology α

Proof state:
case refine_1.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f y < f a✝
h₂ : ¬f y < f x✝
⊢ ∃ y_1 < a✝, f y ≤ f y_1

Tactic:
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
⊢ induced f t = Preorder.topology α

Tactic:
refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y < a✝, b✝ ≤ f y

case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y < a✝, b✝ ≤ f y

Tactic:
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩

Result:
case refine_1.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f y < f a✝
h₂ : ¬f y < f x✝
⊢ ∃ y_1 < a✝, f y ≤ f y_1

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝

Tactic:
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩

Result:
case refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f a✝ < f y
h₂ : ¬f x✝ < f y
⊢ ∃ y_1, a✝ < y_1 ∧ f y_1 ≤ f y

Proof state:
case refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f a✝ < f y
h₂ : ¬f x✝ < f y
⊢ ∃ y_1, a✝ < y_1 ∧ f y_1 ≤ f y

Tactic:
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma surjOn_of_injOn_of_card_le (f : α → β) (hf : Set.MapsTo f s t) (hinj : Set.InjOn f s)
    (hst : #t ≤ #s) : Set.SurjOn f s t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ Set.SurjOn f ↑s ↑t

Tactic:
classical
suffices s.image f = t by simp [← this, Set.SurjOn]
have : s.image f ⊆ t := by aesop (add simp Finset.subset_iff)
exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s = t
⊢ Set.SurjOn f ↑s ↑t

Tactic:
simp [← this, Set.SurjOn]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ Set.SurjOn f ↑s ↑t

Tactic:
suffices s.image f = t by simp [← this, Set.SurjOn]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ image f s = t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s ⊆ t
⊢ image f s = t

Tactic:
exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ image f s = t

Tactic:
have : s.image f ⊆ t := by aesop (add simp Finset.subset_iff)

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s ⊆ t
⊢ image f s = t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ image f s ⊆ t

Tactic:
aesop (add simp Finset.subset_iff)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mergeSort_zipIdx {l : List α} :
    (mergeSort (l.zipIdx) (zipIdxLE le)).map (·.1) = mergeSort l le :=
  go 0 l
where go : ∀ (i : Nat) (l : List α),
    (mergeSort (l.zipIdx i) (zipIdxLE le)).map (·.1) = mergeSort l le
  | _, []
  | _, [a] => by simp [mergeSort]
  | _, a :: b :: xs => by
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1

Proof state:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
⊢ map (fun x => x.fst) (((a :: b :: xs).zipIdx x✝).mergeSort (zipIdxLE le)) = (a :: b :: xs).mergeSort le

Tactic:
have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega

Result:
α : Type u_1
le : α → α → Bool
l : List α
x✝ : Nat
a b : α
xs : List α
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ map (fun x => x.fst) (((a :: b :: xs).zipIdx x✝).mergeSort (zipIdxLE le)) = (a :: b :: xs).mergeSort le
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.inv (huv : u ~[l] v) : (fun x ↦ (u x)⁻¹) ~[l] fun x ↦ (v x)⁻¹

Proof state:
case intro.intro
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1⁻¹)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹

Tactic:
refine ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by norm_num), ?_⟩

Result:
case intro.intro
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ (fun x => (u x)⁻¹) =ᶠ[l] (fun x => (φ x)⁻¹) * fun x => (v x)⁻¹

Proof state:
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹

Tactic:
rcases huv with ⟨φ, hφ, h⟩

Result:
case intro.intro
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹

Proof state:
case intro.intro
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ (fun x => (u x)⁻¹) =ᶠ[l] (fun x => (φ x)⁻¹) * fun x => (v x)⁻¹

Tactic:
convert h.inv

Result:
case h.e'_5.h
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((fun x => (φ x)⁻¹) * fun x => (v x)⁻¹) x✝ = ((φ * v) x✝)⁻¹

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((fun x => (φ x)⁻¹) * fun x => (v x)⁻¹) x✝ = ((φ * v) x✝)⁻¹

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x => (u x)⁻¹) ~[l] fun x => (v x)⁻¹

Tactic:
rw [isEquivalent_iff_exists_eq_mul] at *

Result:
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹

Proof state:
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ 1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹

Tactic:
rw [← inv_one]

Result:
case intro.intro
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1⁻¹)), (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_eq_empty_iff {l₁ : Array α} {l₂ : Array β} :
    zip l₁ l₂ = #[] ↔ l₁ = #[] ∨ l₂ = #[]

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
⊢ { toList := toList✝ }.zip l₂ = #[] ↔ { toList := toList✝ } = #[] ∨ l₂ = #[]

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ { toList := toList✝¹ }.zip { toList := toList✝ } = #[] ↔ { toList := toList✝¹ } = #[] ∨ { toList := toList✝ } = #[]

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ { toList := toList✝¹ }.zip { toList := toList✝ } = #[] ↔ { toList := toList✝¹ } = #[] ∨ { toList := toList✝ } = #[]

Tactic:
simp [List.zip_eq_nil_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
⊢ l₁.zip l₂ = #[] ↔ l₁ = #[] ∨ l₂ = #[]

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
⊢ { toList := toList✝ }.zip l₂ = #[] ↔ { toList := toList✝ } = #[] ∨ l₂ = #[]
-- Mathlib/Data/PNat/Basic.lean
theorem add_sub_of_lt {a b : ℕ+} : a < b → a + (b - a) = b :=
  fun h =>
    PNat.eq <| by
      rw [add_coe, sub_coe, if_pos h]
      exact add_tsub_cancel_of_le h.le

Proof state:
a b : ℕ+
h : a < b
⊢ ↑(a + (b - a)) = ↑b

Tactic:
rw [add_coe, sub_coe, if_pos h]

Result:
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b

Proof state:
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b

Tactic:
exact add_tsub_cancel_of_le h.le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem nodup_insertRatUnits {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) :
    ∀ i : Fin (f.insertRatUnits units).1.ratUnits.size, ∀ j : Fin (f.insertRatUnits units).1.ratUnits.size,
      i ≠ j → (f.insertRatUnits units).1.ratUnits[i] ≠ (f.insertRatUnits units).1.ratUnits[j]

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_eq_k2 : i = k2
⊢ False

Tactic:
rw [← i_eq_k2, hi, bi_eq_true] at h2

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_ne_k1 : ¬i = k1
i_eq_k2 : i = k2
⊢ False

Proof state:
case mk.mk
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRatUnits units).fst.ratUnits[j] = (lj, bj)
heq : (li, bi) = (lj, bj)
⊢ False

Tactic:
cases heq

Result:
case mk.mk.refl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem ite_congr {x y u v : α} {s : Decidable b} [Decidable c]
    (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : ite b x y = ite c u v

Proof state:
case inr
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
⊢ ite b x y = ite c u v

Tactic:
rw [if_neg h]

Result:
case inr
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
⊢ ite b x y = v

Proof state:
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ ite c x y = v

Tactic:
rw [if_neg h]

Result:
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ y = v

Proof state:
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ x = u

Tactic:
exact h₂ h

Result:
no goals

Proof state:
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ y = v

Tactic:
exact h₃ h

Result:
no goals

Proof state:
case inl
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
⊢ ite b x y = ite c u v

Tactic:
rw [if_pos h]

Result:
case inl
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
⊢ ite b x y = u

Proof state:
case inr
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
⊢ ite b x y = v

Tactic:
subst b

Result:
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ ite c x y = v

Proof state:
case inl
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
⊢ ite b x y = u

Tactic:
subst b

Result:
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ ite c x y = u

Proof state:
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
⊢ ite b x y = ite c u v

Tactic:
cases Decidable.em c with
| inl h => rw [if_pos h]; subst b; rw [if_pos h]; exact h₂ h
| inr h => rw [if_neg h]; subst b; rw [if_neg h]; exact h₃ h

Result:
no goals

Proof state:
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ ite c x y = u

Tactic:
rw [if_pos h]

Result:
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ x = u
-- Mathlib/Data/Setoid/Partition.lean
theorem eqv_classes_of_disjoint_union {c : Set (Set α)} (hu : Set.sUnion c = @Set.univ α)
    (H : c.PairwiseDisjoint id) (a) : ∃! b ∈ c, a ∈ b :=
  let ⟨b, hc, ha⟩ := Set.mem_sUnion.1 <| show a ∈ _ by rw [hu]; exact Set.mem_univ a
  ExistsUnique.intro b ⟨hc, ha⟩ fun _ hc' => H.elim_set hc'.1 hc _ hc'.2 ha

Proof state:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ Set.univ

Tactic:
exact Set.mem_univ a

Result:
no goals

Proof state:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ ⋃₀ c

Tactic:
rw [hu]

Result:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ Set.univ
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_whiskerLeft {p f g h pf pfg : C} {η : g ≅ h}
    (η_f : p ⊗ f ≅ pf) (η_fg : pf ⊗ g ≅ pfg) (η_fh : (pf ⊗ h) ≅ pfg)
    (ih_η : pf ◁ η ≪≫ η_fh = η_fg) :
    p ◁ (f ◁ η) ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Tactic:
apply Iso.ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom

Tactic:
simp [← whisker_exchange_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
rw [← ih_η]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype
    {e : PartialHomeomorph M H} (he : e ∈ atlas H M)
    (hs : Nonempty e.source) [HasGroupoid M G] [ClosedUnderRestriction G] :
    let s := { carrier := e.source, is_open' := e.open_source : Opens M }
    let t := { carrier := e.target, is_open' := e.open_target : Opens H }
    ∀ c' ∈ atlas H t, e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ G.maximalAtlas s

Proof state:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : PartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this
⊢ goal.source = (e.subtypeRestr hs).source

Tactic:
simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
  Homeomorph.toPartialHomeomorph_source, toFun_eq_coe, Homeomorph.toPartialHomeomorph_apply,
  Opens.partialHomeomorphSubtypeCoe_source, preimage_univ, inter_self, subtypeRestr_source,
  goal, s]

Result:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : PartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this
⊢ univ = Subtype.val ⁻¹' e.source
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_mul_coeIdeal_eq_coeIdeal {I J : Ideal R₁} {z : K} :
    spanSingleton R₁⁰ z * (I : FractionalIdeal R₁⁰ K) = J ↔
      Ideal.span {((IsLocalization.sec R₁⁰ z).1 : R₁)} * I =
        Ideal.span {((IsLocalization.sec R₁⁰ z).2 : R₁)} * J

Proof state:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
z : K
⊢ spanSingleton R₁⁰ z * ↑I = ↑J ↔ Ideal.span {(sec R₁⁰ z).1} * I = Ideal.span {↑(sec R₁⁰ z).2} * J

Tactic:
rw [← mk'_mul_coeIdeal_eq_coeIdeal K (IsLocalization.sec R₁⁰ z).2.prop,
  IsLocalization.mk'_sec K z]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem newton_seq_dist {n k : ℕ} (hnk : n ≤ k) :
    ‖newton_seq k - newton_seq n‖ ≤ ‖F.derivative.eval a‖ * T ^ 2 ^ n

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
have hex : ∃ m, k = n + m := Nat.exists_eq_add_of_le hnk

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
rw [hex']

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq (n + w✝) - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq (n + w✝) - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
apply newton_seq_dist_aux

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
let ⟨_, hex'⟩ := hex

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n