harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/Rat.lean
theorem Nat.dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y

Proof state:
x y : ℕ
⊢ dist ↑x ↑y = dist x y

Tactic:
rw [← Nat.dist_cast_real, ← Rat.dist_cast]

Result:
x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Proof state:
x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Tactic:
congr

Result:
no goals
-- Mathlib/Data/List/Basic.lean
/-- Consider two lists `l₁` and `l₂` with designated elements `a₁` and `a₂` somewhere in them:
`l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`.
Assume the designated element `a₂` is present in neither `x₁` nor `z₁`.
We conclude that the lists are equal (`l₁ = l₂`) if and only if their respective parts are equal
(`x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂`). -/
lemma append_cons_inj_of_not_mem {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α}
    (notin_x : a₂ ∉ x₁) (notin_z : a₂ ∉ z₁) :
    x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Proof state:
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
constructor

Result:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂

Proof state:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ ((∃ a', x₂ = x₁ ++ a' ∧ (a' = [] ∧ a₂ = a₁ ∧ z₂ = z₁ ∨ ∃ a'_1, a' = a₁ :: a'_1 ∧ z₁ = a'_1 ++ a₂ :: z₂)) ∨
      ∃ c', x₁ = x₂ ++ c' ∧ (c' = [] ∧ a₁ = a₂ ∧ z₁ = z₂ ∨ ∃ a', c' = a₂ :: a' ∧ z₂ = a' ++ a₁ :: z₁)) →
    x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
rintro (⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩ |
  ⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩) <;> simp_all

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u
x₁ z₁ : List α
a₁ : α
notin_x : ¬a₁ ∈ x₁
notin_z : ¬a₁ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₁ ++ a₁ :: z₁

Tactic:
rfl

Result:
no goals

Proof state:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
simp only [append_eq_append_iff, cons_eq_append_iff, cons_eq_cons]

Result:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ ((∃ a', x₂ = x₁ ++ a' ∧ (a' = [] ∧ a₂ = a₁ ∧ z₂ = z₁ ∨ ∃ a'_1, a' = a₁ :: a'_1 ∧ z₁ = a'_1 ++ a₂ :: z₂)) ∨
      ∃ c', x₁ = x₂ ++ c' ∧ (c' = [] ∧ a₁ = a₂ ∧ z₁ = z₂ ∨ ∃ a', c' = a₂ :: a' ∧ z₂ = a' ++ a₁ :: z₁)) →
    x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Proof state:
case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂

Tactic:
rintro ⟨rfl, rfl, rfl⟩

Result:
case mpr.intro.intro
α : Type u
x₁ z₁ : List α
a₁ : α
notin_x : ¬a₁ ∈ x₁
notin_z : ¬a₁ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₁ ++ a₁ :: z₁
-- Mathlib/Data/Fintype/Option.lean
theorem Finite.induction_empty_option {P : Type u → Prop} (of_equiv : ∀ {α β}, α ≃ β → P α → P β)
    (h_empty : P PEmpty) (h_option : ∀ {α} [Fintype α], P α → P (Option α)) (α : Type u)
    [Finite α] : P α

Proof state:
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
⊢ P α

Tactic:
cases nonempty_fintype α

Result:
case intro
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P α

Proof state:
case intro
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P α

Tactic:
refine Fintype.induction_empty_option ?_ ?_ ?_ α

Result:
case intro.refine_1
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β

case intro.refine_2
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P PEmpty.{u + 1}

case intro.refine_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

Proof state:
case intro.refine_1
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β

case intro.refine_2
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P PEmpty.{u + 1}

case intro.refine_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

Tactic:
exacts [fun α β _ => of_equiv, h_empty, @h_option]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem sin_surjective : Function.Surjective sin

Proof state:
case intro
z : ℂ
⊢ ∃ a, sin a = cos z

Tactic:
exact ⟨z + π / 2, sin_add_pi_div_two z⟩

Result:
no goals

Proof state:
⊢ Function.Surjective sin

Tactic:
intro x

Result:
x : ℂ
⊢ ∃ a, sin a = x

Proof state:
x : ℂ
⊢ ∃ a, sin a = x

Tactic:
rcases cos_surjective x with ⟨z, rfl⟩

Result:
case intro
z : ℂ
⊢ ∃ a, sin a = cos z
-- Mathlib/Data/Finset/Insert.lean
theorem insert_val_of_not_mem {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).1 = a ::ₘ s.1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).val = a ::ₘ s.val

Tactic:
rw [insert_val, ndinsert_of_not_mem h]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem qParam_left_inv_mod_period (hh : h ≠ 0) (z : ℂ) :
    ∃ m : ℤ, invQParam h (𝕢 h z) = z + m * h

Proof state:
h : ℝ
hh : h ≠ 0
z : ℂ
⊢ ∃ m, invQParam h (𝕢 h z) = z + ↑m * ↑h

Tactic:
dsimp only [qParam, invQParam]

Result:
h : ℝ
hh : h ≠ 0
z : ℂ
⊢ ∃ m, ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h

Proof state:
case intro
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ∃ m, ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h

Tactic:
refine ⟨m, by rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
  div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]⟩

Result:
no goals

Proof state:
h : ℝ
hh : h ≠ 0
z : ℂ
⊢ ∃ m, ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h

Tactic:
obtain ⟨m, hm⟩ := log_exp_exists (2 * ↑π * I * z / ↑h)

Result:
case intro
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ∃ m, ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h

Proof state:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h

Tactic:
rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_biInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), α) (hf : ∀ i hi, u (l (f i hi)) = f i hi) :
    l (⨅ (i) (hi), f i hi) = ⨅ (i) (hi), l (f i hi)

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)

Tactic:
rw [iInf_subtype', iInf_subtype']

Result:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ x, f ↑x ⋯) = ⨅ x, l (f ↑x ⋯)

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ x, f ↑x ⋯) = ⨅ x, l (f ↑x ⋯)

Tactic:
exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma map_prodMkRight (κ : Kernel α β) (γ : Type*) {mγ : MeasurableSpace γ} (f : β → δ) :
    map (prodMkRight γ κ) f = prodMkRight γ (map κ f)

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ (prodMkRight γ κ).mapOfMeasurable f ⋯ = prodMkRight γ (κ.mapOfMeasurable f ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

Tactic:
simp only [map, hf, ↓reduceDIte]

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ (prodMkRight γ κ).mapOfMeasurable f ⋯ = prodMkRight γ (κ.mapOfMeasurable f ⋯)

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : ¬Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

Tactic:
simp [map_of_not_measurable _ hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : ¬Measurable f
⊢ (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_eq_zero_iff {a b : Tropical (WithTop R)} : a + b = 0 ↔ a = 0 ∧ b = 0

Proof state:
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0

Tactic:
rw [add_eq_iff]

Result:
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0

Proof state:
case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0

Tactic:
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)

Result:
case mp.inl.intro
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0

case mp.inr.intro
R : Type u
inst✝ : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ 0 = 0

Proof state:
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0

case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a

Proof state:
case mp.inr.intro
R : Type u
inst✝ : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ 0 = 0

Tactic:
exact ⟨le_antisymm (le_zero _) h, rfl⟩

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mpr.intro
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0

Proof state:
case mp.inl.intro
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0

Tactic:
exact ⟨rfl, le_antisymm (le_zero _) h⟩

Result:
no goals

Proof state:
case mpr.intro
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_sub_left : neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g₁ g₂ : α →₀ N
⊢ (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂

Tactic:
simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_zero_right (i : ℤ) : lcm i 0 = 0

Proof state:
i : ℤ
⊢ i.natAbs.lcm (natAbs 0) = 0

Tactic:
apply Nat.lcm_zero_right

Result:
no goals

Proof state:
i : ℤ
⊢ i.lcm 0 = 0

Tactic:
rw [Int.lcm]

Result:
i : ℤ
⊢ i.natAbs.lcm (natAbs 0) = 0
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[simp]
lemma preimage_opensRange {X Y : Scheme.{u}} (f : X.Hom Y) [IsOpenImmersion f] :
    f ⁻¹ᵁ f.opensRange = ⊤

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : IsOpenImmersion f
⊢ f ⁻¹ᵁ f.opensRange = ⊤

Tactic:
simp [Scheme.Hom.opensRange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List ((a : α) × β a)} {k : α}
    (h : (l.map Sigma.fst).contains k = false) :
    (insertMany empty l).1.getKey! k = default

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ empty.getKey! k = default

Tactic:
apply getKey!_empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ (empty.insertMany l).val.getKey! k = default

Tactic:
rw [getKey!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ empty.getKey! k = default
-- Mathlib/Data/List/SplitBy.lean
theorem chain'_of_mem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α}
    (hga : ∀ b ∈ g.head?, r b a) (hg : g.Chain' fun y x ↦ r x y)
    (h : m ∈ splitBy.loop r l a g []) : m.Chain' fun x y ↦ r x y

Proof state:
case cons.h_1
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
apply IH _ (chain'_cons'.2 ⟨hga, hg⟩) h

Result:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true
-- Mathlib/Data/Num/Lemmas.lean
theorem ofZNum'_toNat : ∀ n : ZNum, (↑) <$> ofZNum' n = Int.toNat' n
  | 0 => rfl
  | ZNum.pos p => show _ = Int.toNat' p by rw [← PosNum.to_nat_to_int p]; rfl
  | ZNum.neg p =>
    (congr_arg fun x => Int.toNat' (-x)) <|
      show ((p.pred' + 1 : ℕ) : ℤ) = p by rw [← succ'_to_nat]; simp

Proof state:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑p).toNat'

Tactic:
rw [← PosNum.to_nat_to_int p]

Result:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑↑p).toNat'

Proof state:
p : PosNum
⊢ ↑(↑p.pred' + 1) = ↑p

Tactic:
rw [← succ'_to_nat]

Result:
p : PosNum
⊢ ↑↑p.pred'.succ' = ↑p

Proof state:
p : PosNum
⊢ ↑↑p.pred'.succ' = ↑p

Tactic:
simp

Result:
no goals

Proof state:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑↑p).toNat'

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pos_of_mul_pos_left {a b : Nat} (h : 0 < a * b) : 0 < b

Proof state:
case a
a b : Nat
h : 0 < a * b
⊢ ¬0 < b → False

Tactic:
intros

Result:
case a
a b : Nat
h : 0 < a * b
a✝ : ¬0 < b
⊢ False

Proof state:
a b : Nat
h : 0 < a * b
⊢ 0 < b

Tactic:
apply Decidable.by_contra

Result:
case a
a b : Nat
h : 0 < a * b
⊢ ¬0 < b → False

Proof state:
case a
a b : Nat
h : 0 < a * b
a✝ : ¬0 < b
⊢ False

Tactic:
simp_all

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem forall_leftMoves_fuzzy_iff_equiv_zero : (∀ i, G.moveLeft i ‖ 0) ↔ G ≈ 0

Proof state:
case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.LeftMoves
⊢ G.moveLeft i ‖ 0

Tactic:
rw [fuzzy_zero_iff_lf]

Result:
case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.LeftMoves
⊢ G.moveLeft i ⧏ 0

Proof state:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (i : G.LeftMoves), G.moveLeft i ‖ 0
⊢ G ≈ 0

Tactic:
rw [equiv_zero_iff_le G, le_zero_lf]

Result:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (i : G.LeftMoves), G.moveLeft i ‖ 0
⊢ ∀ (i : G.LeftMoves), G.moveLeft i ⧏ 0

Proof state:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (i : G.LeftMoves), G.moveLeft i ‖ 0
⊢ ∀ (i : G.LeftMoves), G.moveLeft i ⧏ 0

Tactic:
exact fun i => (hb i).1

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ (∀ (i : G.LeftMoves), G.moveLeft i ‖ 0) ↔ G ≈ 0

Tactic:
refine ⟨fun hb => ?_, fun hp i => ?_⟩

Result:
case refine_1
G : PGame
inst✝ : G.Impartial
hb : ∀ (i : G.LeftMoves), G.moveLeft i ‖ 0
⊢ G ≈ 0

case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.LeftMoves
⊢ G.moveLeft i ‖ 0

Proof state:
case refine_2
G : PGame
inst✝ : G.Impartial
hp : G ≈ 0
i : G.LeftMoves
⊢ G.moveLeft i ⧏ 0

Tactic:
exact hp.1.moveLeft_lf i

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem mem_fintype_prod [Fintype ι] (f : ι → Set α) (a : α) :
    (a ∈ ∏ i, f i) ↔ ∃ (g : ι → α) (_ : ∀ i, g i ∈ f i), ∏ i, g i = a

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ Finset.univ → g i ∈ f i), ∏ i : ι, g i = a) ↔
    ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i : ι, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a

Tactic:
rw [mem_finset_prod]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ Finset.univ → g i ∈ f i), ∏ i : ι, g i = a) ↔
    ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_add_eq_tsub_right (a c b : α) : a + c - (b + c) = a - b

Proof state:
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a ≤ a + c - (b + c) + b

Tactic:
apply le_of_add_le_add_right

Result:
case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?a ≤ a + c - (b + c) + b + ?a

case a
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α

Proof state:
case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?bc.c ≤ a + c - (b + c) + (b + ?bc.c)

case bc.c
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α

Tactic:
exact le_tsub_add

Result:
no goals

Proof state:
case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?a ≤ a + c - (b + c) + b + ?a

case a
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α

Tactic:
rw [add_assoc]

Result:
case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?bc.c ≤ a + c - (b + c) + (b + ?bc.c)

case bc.c
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α

Proof state:
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + c - (b + c) = a - b

Tactic:
refine add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)

Result:
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a ≤ a + c - (b + c) + b
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c₄_of_char_three : W.c₄ = W.b₂ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₂ ^ 2 - 24 * W.b₄ = W.b₂ ^ 2

Tactic:
linear_combination -8 * W.b₄ * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.c₄ = W.b₂ ^ 2

Tactic:
rw [c₄]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₂ ^ 2 - 24 * W.b₄ = W.b₂ ^ 2