harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean
lemma hom_ext {Z : C} {φ φ' : X₂ ⟶ Z}
    (h₀ : f ≫ φ = f ≫ φ') (h : ∀ i, c.cell i ≫ φ = c.cell i ≫ φ') :
    φ = φ'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ φ = φ'

Tactic:
apply c.isPushout.hom_ext h₀

Result:
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ c.g₂ ≫ φ = c.g₂ ≫ φ'

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ ∀ (i : c.ι), c.cofan₂.inj i ≫ c.g₂ ≫ φ = c.cofan₂.inj i ≫ c.g₂ ≫ φ'

Tactic:
simpa [cell_def] using h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ c.g₂ ≫ φ = c.g₂ ≫ φ'

Tactic:
apply Cofan.IsColimit.hom_ext c.isColimit₂

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ ∀ (i : c.ι), c.cofan₂.inj i ≫ c.g₂ ≫ φ = c.cofan₂.inj i ≫ c.g₂ ≫ φ'
-- Mathlib/Topology/Order/Compact.lean
theorem Continuous.exists_forall_le [ClosedIicTopology α] [Nonempty β] {f : β → α}
    (hf : Continuous f) (hlim : Tendsto f (cocompact β) atTop) : ∃ x, ∀ y, f x ≤ f y

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
inhabit β

Result:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ x, ∀ (y : β), f x ≤ f y
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem exists_aleph {c : Cardinal} : ℵ₀ ≤ c ↔ ∃ o, c = ℵ_ o :=
  ⟨fun h =>
    ⟨preAleph.symm c - ω, by
      rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]
      rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]⟩,
    fun ⟨o, e⟩ => e.symm ▸ aleph0_le_aleph _⟩

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = ℵ_ (preAleph.symm c - ω)

Tactic:
rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]

Result:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ preAleph.symm c

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ preAleph.symm c

Tactic:
rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_eq_floor (a b : α) : toIcoDiv hp a b = ⌊(b - a) / p⌋

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)

Tactic:
rw [Set.mem_Ico, zsmul_eq_mul, ← sub_nonneg, add_comm, sub_right_comm, ← sub_lt_iff_lt_add,
  sub_right_comm _ _ a]

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - ↑⌊(b - a) / p⌋ * p ∧ b - a - ↑⌊(b - a) / p⌋ * p < p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b = ⌊(b - a) / p⌋

Tactic:
refine toIcoDiv_eq_of_sub_zsmul_mem_Ico hp ?_

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - ↑⌊(b - a) / p⌋ * p ∧ b - a - ↑⌊(b - a) / p⌋ * p < p

Tactic:
exact ⟨Int.sub_floor_div_mul_nonneg _ hp, Int.sub_floor_div_mul_lt _ hp⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inrCompHomotopy_hom_desc_hom (hc : ∀ j, ∃ i, c.Rel i j) (i j : ι) :
    (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Proof state:
case pos
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
simp only [inrCompHomotopy_hom φ hc i j hij, desc_f φ α hα _ _ hij,
  comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : ¬c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
simp only [Homotopy.zero _ _ _ hij, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
by_cases hij : c.Rel j i

Result:
case pos
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

case neg
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : ¬c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem add_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs' + rhs' = lhs + rhs

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' + rhs' = lhs + rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma fromOpcycles_op_cyclesOpIso_inv [S.HasRightHomology]:
    S.fromOpcycles.op ≫ S.cyclesOpIso.inv = S.op.toCycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.fromOpcycles.op ≫ S.cyclesOpIso.inv = S.op.toCycles

Tactic:
dsimp [cyclesOpIso, fromOpcycles]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.cyclesIso.inv = S.op.toCycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.cyclesIso.inv = S.op.toCycles

Tactic:
rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
  LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
  ← op_comp, RightHomologyData.p_g', op_f]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitePos_of_tendsto_top {f : ℕ → ℝ} (hf : Tendsto f atTop atTop) :
    InfinitePos (ofSeq f) := fun r =>
  have hf' := tendsto_atTop_atTop.mp hf
  let ⟨i, hi⟩ := hf' (r + 1)
  have hi' : ∀ a : ℕ, f a < r + 1 → a < i := fun a => lt_imp_lt_of_le_imp_le (hi a)
  have hS : { a : ℕ | r < f a }ᶜ ⊆ { a : ℕ | a ≤ i }

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | f a ≤ r} ⊆ {a | a ≤ i}

Tactic:
exact fun a har => le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _)))

Result:
no goals

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | r < f a}ᶜ ⊆ {a | a ≤ i}

Tactic:
simp only [Set.compl_setOf, not_lt]

Result:
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | f a ≤ r} ⊆ {a | a ≤ i}
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem sphere_subset_preimage_metric_sphere : (sphere n d k : Set (Fin n → ℕ)) ⊆
    (fun x : Fin n → ℕ => (WithLp.equiv 2 _).symm ((↑) ∘ x : Fin n → ℝ)) ⁻¹'
      Metric.sphere (0 : PiLp 2 fun _ : Fin n => ℝ) (√↑k) :=
  fun x hx => by rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]

Proof state:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ ↑(sphere n d k)
⊢ x ∈ (fun x => (WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 √↑k

Tactic:
rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.comp_contDiffAt_iff (e : F ≃L[𝕜] G) :
    ContDiffAt 𝕜 n (e ∘ f) x ↔ ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : F ≃L[𝕜] G
⊢ ContDiffAt 𝕜 n (⇑e ∘ f) x ↔ ContDiffAt 𝕜 n f x

Tactic:
simp only [← contDiffWithinAt_univ, e.comp_contDiffWithinAt_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem _root_.DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ}
    {f : ℂ → E} (hf : DiffContOnCl ℂ f (ball c R)) (hw : w ∈ ball c R) :
    ((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

Tactic:
have hR : 0 < R := not_le.mp (ball_eq_empty.not.mp (Set.nonempty_of_mem hw).ne_empty)

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

Proof state:
case refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ContinuousOn f (closedBall c R)

Tactic:
simpa only [closure_ball c hR.ne.symm] using hf.continuousOn

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w

Tactic:
refine two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  countable_empty hw ?_ ?_

Result:
case refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ContinuousOn f (closedBall c R)

case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x

Proof state:
case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x

Tactic:
simpa only [diff_empty] using fun z hz => hf.differentiableAt isOpen_ball hz

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_append_right :
    ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
  | [],     _, _ => rfl
  | _ :: _, _, h => by
    simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]

Proof state:
α : Type u_1
p : α → Bool
head✝ : α
tail✝ x✝ : List α
h : ∀ (b : α), b ∈ head✝ :: tail✝ → ¬p b = true
⊢ eraseP p (head✝ :: tail✝ ++ x✝) = head✝ :: tail✝ ++ eraseP p x✝

Tactic:
simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]

Result:
no goals
-- Mathlib/Topology/Instances/Matrix.lean
theorem Continuous.matrix_fromBlocks {A : X → Matrix n l R} {B : X → Matrix n m R}
    {C : X → Matrix p l R} {D : X → Matrix p m R} (hA : Continuous A) (hB : Continuous B)
    (hC : Continuous C) (hD : Continuous D) :
    Continuous fun x => Matrix.fromBlocks (A x) (B x) (C x) (D x) :=
  continuous_matrix <| by
    rintro (i | i) (j | j) <;> refine Continuous.matrix_elem ?_ i j <;> assumption

Proof state:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
⊢ ∀ (i : n ⊕ p) (j : l ⊕ m), Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) i j

Tactic:
rintro (i | i) (j | j) <;> refine Continuous.matrix_elem ?_ i j <;> assumption

Result:
no goals
-- Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean
theorem aemeasurable_of_re_im (hre : AEMeasurable (fun x => RCLike.re (f x)) μ)
    (him : AEMeasurable (fun x => RCLike.im (f x)) μ) : AEMeasurable f μ

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (fun x => RCLike.re (f x)) μ
him : AEMeasurable (fun x => RCLike.im (f x)) μ
⊢ AEMeasurable f μ

Tactic:
convert AEMeasurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp_aemeasurable hre)
    ((RCLike.measurable_ofReal.comp_aemeasurable him).mul_const RCLike.I)

Result:
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (fun x => RCLike.re (f x)) μ
him : AEMeasurable (fun x => RCLike.im (f x)) μ
x✝ : α
⊢ f x✝ = (RCLike.ofReal ∘ fun x => RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x => RCLike.im (f x)) x✝ * RCLike.I

Proof state:
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (fun x => RCLike.re (f x)) μ
him : AEMeasurable (fun x => RCLike.im (f x)) μ
x✝ : α
⊢ f x✝ = (RCLike.ofReal ∘ fun x => RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x => RCLike.im (f x)) x✝ * RCLike.I

Tactic:
exact (RCLike.re_add_im _).symm

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma inv_lt_one_iff₀ : a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

Tactic:
simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_zero {x : AddCircle T} : fourier 0 x = 1

Proof state:
T : ℝ
x : AddCircle T
⊢ (fourier 0) x = 1

Tactic:
induction x using QuotientAddGroup.induction_on

Result:
case H
T z✝ : ℝ
⊢ (fourier 0) ↑z✝ = 1

Proof state:
case H
T z✝ : ℝ
⊢ Complex.exp (2 * ↑π * Complex.I * ↑0 * ↑z✝ / ↑T) = 1

Tactic:
norm_num

Result:
no goals

Proof state:
case H
T z✝ : ℝ
⊢ (fourier 0) ↑z✝ = 1

Tactic:
simp only [fourier_coe_apply]

Result:
case H
T z✝ : ℝ
⊢ Complex.exp (2 * ↑π * Complex.I * ↑0 * ↑z✝ / ↑T) = 1
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_div_eq_dist_mul_right (a b c : E) : dist a (b / c) = dist (a * c) b

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
a b c : E
⊢ dist a (b / c) = dist (a * c) b

Tactic:
rw [← dist_mul_right _ _ c, div_mul_cancel]

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {r : R} (hr : r ≠ 0) :
    Squarefree r ↔ ∀ x : R, Irreducible x → ¬x * x ∣ r

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
simpa [hr] using (irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree r).symm

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem monic_denom (x : RatFunc K) : (denom x).Monic

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ x.denom.Monic

Tactic:
classical
induction x using RatFunc.induction_on with
| f p q hq =>
  rw [denom_div p hq, mul_comm]
  exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

Result:
no goals

Proof state:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom.Monic

Tactic:
rw [denom_div p hq, mul_comm]

Result:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (q / gcd p q * C (q / gcd p q).leadingCoeff⁻¹).Monic

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ x.denom.Monic

Tactic:
induction x using RatFunc.induction_on with
| f p q hq =>
  rw [denom_div p hq, mul_comm]
  exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

Result:
no goals

Proof state:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (q / gcd p q * C (q / gcd p q).leadingCoeff⁻¹).Monic

Tactic:
exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

Result:
no goals
-- Mathlib/MeasureTheory/Function/Floor.lean
theorem measurable_fract [BorelSpace R] : Measurable (Int.fract : R → R)

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1))

Tactic:
exact MeasurableSet.iUnion fun z => measurable_id.sub_const _ (hs.inter measurableSet_Ico)

Result:
no goals

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract ⁻¹' s)

Tactic:
rw [Int.preimage_fract]

Result:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1))

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
⊢ Measurable Int.fract

Tactic:
intro s hs

Result:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract ⁻¹' s)
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem prime_X : Prime (X : R[X])

Proof state:
case h.e'_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X = X - C 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
convert prime_X_sub_C (0 : R)

Result:
case h.e'_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X = X - C 0
-- Mathlib/Tactic/Rify.lean
@[rify_simps] lemma ratCast_eq (a b : ℚ) : a = b ↔ (a : ℝ) = (b : ℝ)

Proof state:
a b : ℚ
⊢ a = b ↔ ↑a = ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_balance1 (l : RBNode α) (v : α) (r : RBNode α) :
    (balance1 l v r).reverse = balance2 r.reverse v l.reverse

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance1 v r).reverse = r.reverse.balance2 v l.reverse

Tactic:
unfold balance1 balance2

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b).reverse =
    match r.reverse, v, l.reverse with
    | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
    | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
    | a, x, b => node black a x b
-- Mathlib/Analysis/Complex/Arg.lean
theorem sameRay_iff : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Proof state:
case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Result:
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ x.arg = arg 0

case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Proof state:
case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = y.arg

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑‖x‖ * y = ↑‖y‖ * x ↔ ↑‖y‖ * x = y * ↑‖x‖

Tactic:
rw [mul_comm, eq_comm]

Result:
no goals

Proof state:
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
simp only [hx, hy, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]

Result:
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ False ∨ False ∨ ↑‖y‖ / ↑‖x‖ * x = y

Proof state:
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ x.arg = arg 0

Tactic:
simp

Result:
no goals

Proof state:
x y : ℂ
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = y.arg

case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Proof state:
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ False ∨ False ∨ ↑‖y‖ / ↑‖x‖ * x = y

Tactic:
field_simp [hx, hy]

Result:
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑‖x‖ * y = ↑‖y‖ * x ↔ ↑‖y‖ * x = y * ↑‖x‖
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem nums_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) :
    g.nums m = g.nums n

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.nums m = g.nums n

Tactic:
simp only [num_eq_conts_a, conts_stable_of_terminated n_le_m terminatedAt_n]

Result:
no goals