harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Insert.lean
@[simp] lemma nonempty_compl_of_nontrivial [Nontrivial α] (x : α) : Set.Nonempty {x}ᶜ

Proof state:
α : Type u
inst✝ : Nontrivial α
x y : α
hy : y ≠ x
⊢ y ∈ {x}ᶜ

Tactic:
simp [hy]

Result:
no goals

Proof state:
α : Type u
inst✝ : Nontrivial α
x : α
⊢ {x}ᶜ.Nonempty

Tactic:
obtain ⟨y, hy⟩ := exists_ne x

Result:
case intro
α : Type u
inst✝ : Nontrivial α
x y : α
hy : y ≠ x
⊢ {x}ᶜ.Nonempty

Proof state:
case intro
α : Type u
inst✝ : Nontrivial α
x y : α
hy : y ≠ x
⊢ {x}ᶜ.Nonempty

Tactic:
exact ⟨y, by simp [hy]⟩

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafExt_inv {F G : Profinite.{u}ᵒᵖ ⥤ Type (u+1)} (S : Profinite.{u}ᵒᵖ)
    (i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G) : (lanPresheafExt i).inv.app S =
      colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv)

Proof state:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ (lanPresheafExt i).inv.app S = colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv)

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
  leftKanExtensionUniqueOfIso_inv, pointwiseLeftKanExtension_desc_app]

Result:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
        (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv)

Proof state:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
        (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv)

Tactic:
apply colimit.hom_ext

Result:
case w
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
            (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv)

Proof state:
case w
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ G)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F))
            (i.inv ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ F)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ G) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv)

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_homothety_preimage {d : ℝ} (hd : 0 ≤ d) (x : P) {c : 𝕜} (hc : c ≠ 0)
    (s : Set P) : μH[d] (AffineMap.homothety x c ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s

Proof state:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑((AffineEquiv.homothetyUnitsMulHom x) (Units.mk0 c hc)) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s

Tactic:
rw [← AffineEquiv.image_symm, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm,
  hausdorffMeasure_homothety_image hd x (_ : 𝕜ˣ).isUnit.ne_zero, Units.val_inv_eq_inv_val,
  Units.val_mk0, nnnorm_inv]

Result:
no goals

Proof state:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(AffineMap.homothety x c) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s

Tactic:
change μH[d] (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 c hc) ⁻¹' s) = _

Result:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑((AffineEquiv.homothetyUnitsMulHom x) (Units.mk0 c hc)) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_succ_eq_bot {n : ℕ} (h : lowerCentralSeries G n ≤ center G) :
    lowerCentralSeries G (n + 1) = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ lowerCentralSeries G (n + 1) = ⊥

Tactic:
rw [lowerCentralSeries_succ, closure_eq_bot_iff, Set.subset_singleton_iff]

Result:
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ ∀ y ∈ {x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}, y = 1

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ z * y = y * z

Tactic:
exact mem_center_iff.mp (h hy1) z

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ ∀ y ∈ {x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}, y = 1

Tactic:
rintro x ⟨y, hy1, z, ⟨⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ y * z * y⁻¹ * z⁻¹ = 1

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ y * z * y⁻¹ * z⁻¹ = 1

Tactic:
rw [mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ z * y = y * z
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r)
    (h : ‖logEmbedding K (Additive.ofMul x)‖ ≤ r) (w : InfinitePlace K) :
    |Real.log (w x)| ≤ (Fintype.card (InfinitePlace K)) * r

Proof state:
case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ ↑(#univ) * r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
refine mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg

Result:
case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ ↑(#univ) ≤ ↑(Fintype.card (InfinitePlace K))

Proof state:
case neg.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤
    ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))|

Tactic:
exact tool _ (abs_nonneg _)

Result:
no goals

Proof state:
case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑w.mult * |Real.log (w ((algebraMap (𝓞 K) K) ↑x))|

Tactic:
exact tool _ (abs_nonneg _)

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_singleton (a : α) : filter p {a} = if p a then {a} else ∅

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
⊢ x = a ∧ p x ↔ x ∈ if p a then {a} else ∅

Tactic:
split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']

Result:
no goals

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
⊢ x ∈ filter p {a} ↔ x ∈ if p a then {a} else ∅

Tactic:
simp only [mem_singleton, forall_eq, mem_filter]

Result:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
⊢ x = a ∧ p x ↔ x ∈ if p a then {a} else ∅

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
ext x

Result:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
⊢ x ∈ filter p {a} ↔ x ∈ if p a then {a} else ∅

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
classical
  ext x
  simp only [mem_singleton, forall_eq, mem_filter]
  split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_zero (f : ∀ a < (0 : Ordinal), Ordinal) : blsub 0 f = 0

Proof state:
f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}
⊢ blsub 0 f = 0

Tactic:
rw [blsub_eq_zero_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Defs.lean
lemma Subring.toNonUnitalSubring_toSubring (S : Subring R) :
    S.toNonUnitalSubring.toSubring S.one_mem = S

Proof state:
R : Type u
inst✝ : Ring R
S : Subring R
⊢ S.toNonUnitalSubring.toSubring ⋯ = S

Tactic:
cases S

Result:
case mk
R : Type u
inst✝ : Ring R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }

Proof state:
case mk
R : Type u
inst✝ : Ring R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem mono (h : LiouvilleWith p x) (hle : q ≤ p) : LiouvilleWith q x

Proof state:
case intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ q

Tactic:
rintro n ⟨hn, m, hne, hlt⟩

Result:
case intro.intro.intro.intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ q

Proof state:
case intro.intro.intro.intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ q

Tactic:
refine ⟨m, hne, hlt.trans_le <| ?_⟩

Result:
case intro.intro.intro.intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ C / ↑n ^ q

Proof state:
case intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith q x

Tactic:
refine ⟨C, hC.mono ?_⟩

Result:
case intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ q

Proof state:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
⊢ LiouvilleWith q x

Tactic:
rcases h.exists_pos with ⟨C, hC₀, hC⟩

Result:
case intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith q x

Proof state:
case intro.intro.intro.intro.intro.h.hx
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 1 ≤ ↑n

Tactic:
exact_mod_cast hn

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ C / ↑n ^ q

Tactic:
gcongr

Result:
case intro.intro.intro.intro.intro.h.hx
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 1 ≤ ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem replicate_eq_replicateTR : @List.replicate = @List.replicateTR

Proof state:
case h.h
α : Type u_1
⊢ ∀ (x : Nat), replicate x = replicateTR x

Tactic:
intro n

Result:
case h.h
α : Type u_1
n : Nat
⊢ replicate n = replicateTR n

Proof state:
case h.h.h
α : Type u_1
n : Nat
a : α
⊢ replicate n a = replicateTR n a

Tactic:
exact (replicateTR_loop_replicate_eq _ 0 n).symm

Result:
no goals

Proof state:
case h
α : Type u_1
⊢ replicate = replicateTR

Tactic:
apply funext

Result:
case h.h
α : Type u_1
⊢ ∀ (x : Nat), replicate x = replicateTR x

Proof state:
case h.h
α : Type u_1
n : Nat
⊢ replicate n = replicateTR n

Tactic:
apply funext

Result:
case h.h.h
α : Type u_1
n : Nat
⊢ ∀ (x : α), replicate n x = replicateTR n x

Proof state:
⊢ @replicate = @replicateTR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Type u_1), replicate = replicateTR

Proof state:
case h

⊢ ∀ (x : Type u_1), replicate = replicateTR

Tactic:
intro α

Result:
case h
α : Type u_1
⊢ replicate = replicateTR

Proof state:
case h.h.h
α : Type u_1
n : Nat
⊢ ∀ (x : α), replicate n x = replicateTR n x

Tactic:
intro a

Result:
case h.h.h
α : Type u_1
n : Nat
a : α
⊢ replicate n a = replicateTR n a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_eq_and {a b : BitVec 1} : a * b = a &&& b

Proof state:
a b : BitVec 1
ha : a = 0 ∨ a = 1
hb : b = 0 ∨ b = 1
⊢ a * b = a &&& b

Tactic:
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))

Result:
no goals

Proof state:
case inr
a b : BitVec 1
hb : b = 0 ∨ b = 1
h : a = 1
⊢ a * b = a &&& b

Tactic:
rcases hb with h' | h' <;> (simp [h, h'])

Result:
no goals

Proof state:
case inr.inr
a b : BitVec 1
h : a = 1
h' : b = 1
⊢ a * b = a &&& b

Tactic:
simp [h, h']

Result:
no goals

Proof state:
a b : BitVec 1
ha : a = 0 ∨ a = 1
⊢ a * b = a &&& b

Tactic:
have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _

Result:
a b : BitVec 1
ha : a = 0 ∨ a = 1
hb : b = 0 ∨ b = 1
⊢ a * b = a &&& b

Proof state:
a b : BitVec 1
⊢ a * b = a &&& b

Tactic:
have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _

Result:
a b : BitVec 1
ha : a = 0 ∨ a = 1
⊢ a * b = a &&& b
-- Mathlib/Order/Basic.lean
theorem PartialOrder.ext {A B : PartialOrder α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) : A = B

Proof state:
case a.a.le.h.h.a
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
exact H x y

Result:
no goals

Proof state:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y

Result:
case a.a.le.h.h.a
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ico_top (x : ℝ) : Real.toEReal ⁻¹' Ico x ⊤ = Ici x

Proof state:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ⊤) = Ici x

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
⊢ Real.toEReal ⁻¹' Ico ↑x ⊤ = Ici x

Tactic:
rw [← Ici_inter_Iio]

Result:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ⊤) = Ici x
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_neg_one : log (-1) = π * I

Proof state:
⊢ log (-1) = ↑π * I

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem ListBlank.map_cons {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ')
    (l : ListBlank Γ) (a : Γ) : (l.cons a).map f = (l.map f).cons (f a)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ map f (cons a l) = cons (f.f a) (map f l)

Tactic:
refine (ListBlank.cons_head_tail _).symm.trans ?_

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ cons (map f (cons a l)).head (map f (cons a l)).tail = cons (f.f a) (map f l)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ cons (map f (cons a l)).head (map f (cons a l)).tail = cons (f.f a) (map f l)

Tactic:
simp only [ListBlank.head_map, ListBlank.head_cons, ListBlank.tail_map, ListBlank.tail_cons]

Result:
no goals
-- Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean
theorem hasDerivAt_integral_of_dominated_loc_of_lip {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜}
    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
    (hF_int : IntervalIntegrable (F x₀) μ a b)
    (hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b)))
    (h_lipsch : ∀ᵐ t ∂μ, t ∈ Ι a b →
      LipschitzOnWith (Real.nnabs <| bound t) (fun x => F x t) (ball x₀ ε))
    (bound_integrable : IntervalIntegrable (bound : ℝ → ℝ) μ a b)
    (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → HasDerivAt (fun x => F x t) (F' t) x₀) :
    IntervalIntegrable F' μ a b ∧
      HasDerivAt (fun x => ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun x => F x t) (F' t) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lipsch h_diff

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lipsch : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasDerivAt (fun x_1 => F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp] lemma rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ y⁻¹) ^ y = x

Proof state:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem UniformContinuous.prod_mk {f₁ : α → β} {f₂ : α → γ} (h₁ : UniformContinuous f₁)
    (h₂ : UniformContinuous f₂) : UniformContinuous fun a => (f₁ a, f₂ a)

Proof state:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x => ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun p => (p.1.1, p.2.1)) (𝓤 β) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (𝓤 γ))

Tactic:
exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

Result:
no goals

Proof state:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ UniformContinuous fun a => (f₁ a, f₂ a)

Tactic:
rw [UniformContinuous, uniformity_prod]

Result:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x => ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun p => (p.1.1, p.2.1)) (𝓤 β) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (𝓤 γ))
-- Mathlib/Data/Set/Functor.lean
theorem mem_of_mem_coe {a : α} (ha : a ∈ (γ : Set α)) : ⟨a, coe_subset ha⟩ ∈ γ

Proof state:
α : Type u
β : Set α
γ : Set ↑β
a : α
ha :
  a ∈ do
    let a ← γ
    pure ↑a
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Set α
γ : Set ↑β
a : α
w✝ : ↑β
ha : w✝ ∈ γ
right✝ : a ∈ (fun h => (fun a => pure ↑a) w✝) ha
⊢ ⟨a, ⋯⟩ ∈ γ

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Set α
γ : Set ↑β
a : α
w✝ : ↑β
ha : w✝ ∈ γ
right✝ : a ∈ (fun h => (fun a => pure ↑a) w✝) ha
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
convert ha

Result:
no goals