harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMConfig.lean
theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
    Turing.eval step (stepNormal f (Cont.fix f k) v) =
      f.fix.eval v >>= fun v => Turing.eval step (Cfg.ret k v)

Proof state:
case pos
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₂ ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl v₁.tail) ∧
        v₂ ∈
          PFun.fix (fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'

Tactic:
rw [Part.mem_some_iff.1 hv₂]

Result:
case pos
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₁.tail ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl v₁.tail) ∧
        v₁.tail ∈
          PFun.fix (fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'
-- Mathlib/Data/PNat/Basic.lean
theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ)

Proof state:
case mp.intro
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)

Tactic:
apply dvd_mul_right

Result:
no goals

Proof state:
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
k m : ℕ+
h : ↑m = ↑k * 0
⊢ False

Proof state:
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (n := a) <| by
  rintro rfl
  simp only [mul_zero, ne_zero] at h

Result:
case mpr.intro.intro
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ k ∣ m

Proof state:
k m : ℕ+
h : ↑m = ↑k * 0
⊢ False

Tactic:
simp only [mul_zero, ne_zero] at h

Result:
no goals

Proof state:
case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m

Tactic:
rcases h with ⟨a, h⟩

Result:
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m

Proof state:
case mpr.intro.intro
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ k ∣ m

Tactic:
use ⟨n.succ, n.succ_pos⟩

Result:
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ m = k * ⟨n.succ, ⋯⟩

Proof state:
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ m = k * ⟨n.succ, ⋯⟩

Tactic:
rw [← coe_inj, h, mul_coe, mk_coe]

Result:
no goals

Proof state:
k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m

Tactic:
constructor <;> intro h

Result:
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m

Proof state:
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

Tactic:
rcases h with ⟨_, rfl⟩

Result:
case mp.intro
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)
-- Mathlib/Logic/Function/Basic.lean
lemma FactorsThrough.extend_apply {g : α → γ} (hf : g.FactorsThrough f) (e' : β → γ) (a : α) :
    extend f g e' (f a) = g a

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ g (Classical.choose ⋯) = g a

Tactic:
exact hf (Classical.choose_spec (exists_apply_eq_apply f a))

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a

Tactic:
simp only [extend_def, dif_pos, exists_apply_eq_apply]

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ g (Classical.choose ⋯) = g a
-- Mathlib/Order/Filter/Map.lean
theorem comap_snd_neBot_iff {f : Filter β} :
    (f.comap (Prod.snd : α × β → β)).NeBot ↔ Nonempty α ∧ f.NeBot

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Result:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

case inr
α : Type u_1
β : Type u_2
f : Filter β
hα : Nonempty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Proof state:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Result:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ¬⊥.NeBot ↔ ¬(Nonempty α ∧ f.NeBot)

Proof state:
case inr
α : Type u_1
β : Type u_2
f : Filter β
hα : Nonempty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
simp [comap_neBot_iff_frequently, hα]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ¬⊥.NeBot ↔ ¬(Nonempty α ∧ f.NeBot)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_le_of_eq_bot {I : Ideal R} [I.IsTwoSided] (h : jacobson (R ⧸ I) = ⊥) :
    jacobson R ≤ I :=
  Module.jacobson_le_of_eq_bot <| by
    rw [← le_bot_iff, ← SetLike.coe_subset_coe] at h ⊢
    rwa [← coe_jacobson_quotient]

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : ↑(jacobson (R ⧸ I)) ⊆ ↑⊥
⊢ ↑(Module.jacobson R (R ⧸ I)) ⊆ ↑⊥

Tactic:
rwa [← coe_jacobson_quotient]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : jacobson (R ⧸ I) = ⊥
⊢ Module.jacobson R (R ⧸ I) = ⊥

Tactic:
rw [← le_bot_iff, ← SetLike.coe_subset_coe] at h ⊢

Result:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : ↑(jacobson (R ⧸ I)) ⊆ ↑⊥
⊢ ↑(Module.jacobson R (R ⧸ I)) ⊆ ↑⊥
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem bot_eq_top_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) :
    (⊥ : IntermediateField F E) = ⊤

Proof state:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥

Tactic:
exact finrank_adjoin_simple_eq_one_iff.mp (h y)

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
⊢ ⊥ = ⊤

Tactic:
ext y

Result:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤

Proof state:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤

Tactic:
rw [iff_true_right IntermediateField.mem_top]

Result:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem comap_maximalIdeal (h : IsLocalRing S := isLocalRing S I) :
    (IsLocalRing.maximalIdeal S).comap (algebraMap R S) = I :=
  Ideal.ext fun x => by simpa only [Ideal.mem_comap] using to_map_mem_maximal_iff _ I x

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
h : optParam (IsLocalRing S) ⋯
x : R
⊢ x ∈ Ideal.comap (algebraMap R S) (IsLocalRing.maximalIdeal S) ↔ x ∈ I

Tactic:
simpa only [Ideal.mem_comap] using to_map_mem_maximal_iff _ I x

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι}
    [l.IsCountablyGenerated] {F : ι → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
    (hF_meas : ∀ᶠ n in l, Measurable (F n)) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a)
    (h_fin : ∫⁻ a, bound a ∂μ ≠ ∞) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) :
    Tendsto (fun n => ∫⁻ a, F n a ∂μ) l (𝓝 <| ∫⁻ a, f a ∂μ)

Proof state:
case intro.refine_5.hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => F n a) ?intro.refine_5.y (𝓝 (f a))

Tactic:
assumption

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem Subalgebra.isSimpleOrder_of_finrank (hr : finrank F E = 2) :
    IsSimpleOrder (Subalgebra F E) :=
  let i := nontrivial_of_finrank_pos (zero_lt_two.trans_eq hr.symm)
  { toNontrivial :=
      ⟨⟨⊥, ⊤, fun h => by cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)⟩⟩
    eq_bot_or_eq_top

Proof state:
case «1»
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥ ∨ S = ⊤

Tactic:
left

Result:
case «1».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥

Proof state:
case «1».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥

Tactic:
exact Subalgebra.eq_bot_of_finrank_one h

Result:
no goals
-- Mathlib/Topology/Sheaves/Sheafify.lean
theorem stalkToFiber_injective (x : X) : Function.Injective (F.stalkToFiber x)

Proof state:
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : F.germ U' x ⋯ gU = fV ⟨x, ⋯⟩
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
wUx : fU ⟨x, ⋯⟩ = F.germ U' x ⋯ gU
⊢ ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)

Tactic:
clear wUx

Result:
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : F.germ U' x ⋯ gU = fV ⟨x, ⋯⟩
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
⊢ ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)

Proof state:
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : F.germ U' x ⋯ gU = fV ⟨x, ⋯⟩
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
⊢ ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)

Tactic:
have wVx := wV ⟨x, mV⟩

Result:
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : F.germ U' x ⋯ gU = fV ⟨x, ⋯⟩
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
wVx : (fun x_1 => fV (iV x_1)) ⟨x, mV⟩ = F.germ V' ↑⟨x, mV⟩ ⋯ gV
⊢ ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Classical.lean
theorem em (p : Prop) : p ∨ ¬p :=
  let U (x : Prop) : Prop := x = True ∨ p
  let V (x : Prop) : Prop := x = False ∨ p
  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
  let u : Prop := choose exU
  let v : Prop := choose exV
  have u_def : U u := choose_spec exU
  have v_def : V v := choose_spec exV
  have not_uv_or_p : u ≠ v ∨ p :=
    match u_def, v_def with
    | Or.inr h, _ => Or.inr h
    | _, Or.inr h => Or.inr h
    | Or.inl hut, Or.inl hvf =>
      have hne : u ≠ v

Proof state:
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
exU✝ exV✝ : ∃ x, V x
⊢ choose exU✝ = choose exV✝

Tactic:
rfl

Result:
no goals

Proof state:
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
hut : u = True
hvf : v = False
⊢ u ≠ v

Tactic:
simp [hvf, hut, true_ne_false]

Result:
no goals

Proof state:
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
⊢ ∀ (exU : ∃ x, U x) (exV : ∃ x, V x), choose exU = choose exV

Tactic:
rw [hpred]

Result:
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
⊢ ∀ (exU exV : ∃ x, V x), choose exU = choose exV

Proof state:
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
⊢ ∀ (exU exV : ∃ x, V x), choose exU = choose exV

Tactic:
intros

Result:
p : Prop
U : Prop → Prop := fun x => x = True ∨ p
V : Prop → Prop := fun x => x = False ∨ p
exU : ∃ x, U x
exV : ∃ x, V x
u : Prop := choose exU
v : Prop := choose exV
u_def : U u
v_def : V v
not_uv_or_p : u ≠ v ∨ p
hp : p
hpred : U = V
exU✝ exV✝ : ∃ x, V x
⊢ choose exU✝ = choose exV✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
    (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx1 : idx < w),
        curr ≤ idx
          →
        (go input distance curr hcurr s).get idx hidx1
          =
        if hidx3 : idx < w - distance % w then
          input.get ((distance % w) + idx) (by omega)
        else
          input.get (idx - (w - (distance % w))) (by omega)

Proof state:
case isTrue.inr.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.push (input.get (curr - (w - distance % w)) ⋯))).get idx hidx1 =
    if hidx3 : idx < w - distance % w then input.get (distance % w + idx) ⋯ else input.get (idx - (w - distance % w)) ⋯

Tactic:
rw [go_get]

Result:
case isTrue.inr.isFalse.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ curr + 1 ≤ idx

Proof state:
case isTrue.inl.isTrue.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝² : curr < w
heq : curr = idx
h✝¹ : curr < w - distance % w
h✝ : idx < w - distance % w
⊢ input.get (distance % w + curr) ⋯ = input.get (distance % w + idx) ⋯

Tactic:
simp [heq]

Result:
no goals

Proof state:
case isTrue.inl.isFalse.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝² : curr < w
heq : curr = idx
h✝¹ : ¬curr < w - distance % w
h✝ : ¬idx < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.push (input.get (curr - (w - distance % w)) ⋯))).get idx hidx1 =
    input.get (idx - (w - distance % w)) ⋯

Tactic:
rw [go_get_aux]

Result:
case isTrue.inl.isFalse.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝² : curr < w
heq : curr = idx
h✝¹ : ¬curr < w - distance % w
h✝ : ¬idx < w - distance % w
⊢ (s.push (input.get (curr - (w - distance % w)) ⋯)).get idx ?isTrue.inl.isFalse.isFalse.hidx =
    input.get (idx - (w - distance % w)) ⋯

case isTrue.inl.isFalse.isFalse.hidx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝² : curr < w
heq : curr = idx
h✝¹ : ¬curr < w - distance % w
h✝ : ¬idx < w - distance % w
⊢ idx < curr + 1
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem ae_ae_comm {p : α → β → Prop} (h : MeasurableSet {x : α × β | p x.1 x.2}) :
    (∀ᵐ x ∂μ, ∀ᵐ y ∂ν, p x y) ↔ ∀ᵐ y ∂ν, ∀ᵐ x ∂μ, p x y := calc
  _ ↔ ∀ᵐ x ∂μ.prod ν, p x.1 x.2 := .symm <| ae_prod_iff_ae_ae h
  _ ↔ ∀ᵐ x ∂ν.prod μ, p x.2 x.1

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ AEMeasurable Prod.swap (ν.prod μ)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : α × β) ∂μ.prod ν, p x.1 x.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
rw [← prod_swap, ae_map_iff (by fun_prop) h]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.commute (h : Disjoint f g) : Commute f g :=
  Equiv.ext fun x =>
    (h x).elim
      (fun hf =>
        (h (g x)).elim (fun hg => by simp [mul_apply, hf, hg]) fun hg => by
          simp [mul_apply, hf, g.injective hg])
      fun hg =>
      (h (f x)).elim (fun hf => by simp [mul_apply, f.injective hf, hg]) fun hf => by
        simp [mul_apply, hf, hg]

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : g x = x
hf : g (f x) = f x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, hf, hg]

Result:
no goals

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hf : f x = x
hg : f (g x) = g x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, hf, hg]

Result:
no goals

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hf : f x = x
hg : g (g x) = g x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, hf, g.injective hg]

Result:
no goals

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : g x = x
hf : f (f x) = f x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, f.injective hf, hg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_mul_cos_add_sin_mul_I {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ ∈ Set.Ioc (-π) π) :
    arg (r * (cos θ + sin θ * I)) = θ

Proof state:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ

Result:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Proof state:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ θ < π + π / 2

Tactic:
linarith

Result:
no goals

Proof state:
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
replace hθ := hθ.2

Result:
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Proof state:
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [if_pos]

Result:
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ Real.arcsin (Real.sin θ) = θ

case pos.hc
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ Real.cos θ
-- Mathlib/Topology/Bases.lean
theorem _root_.Dense.isSeparable_iff (hs : Dense s) :
    IsSeparable s ↔ SeparableSpace α

Proof state:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsSeparable s ↔ SeparableSpace α

Tactic:
simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
  ← hs.closure_eq, isClosed_closure.closure_subset_iff]

Result:
no goals