harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem MemLp.integrable_norm_rpow' [IsFiniteMeasure μ] {f : α → β} {p : ℝ≥0∞} (hf : MemLp f p μ) :
    Integrable (fun x : α => ‖f x‖ ^ p.toReal) μ

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : p = ⊤
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Tactic:
simp [h_top, integrable_const]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : p = 0
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Tactic:
simp [h_zero, integrable_const]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : p = ⊤
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : ¬p = ⊤
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
h_top : ¬p = ⊤
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Tactic:
exact hf.integrable_norm_rpow h_zero h_top

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Tactic:
by_cases h_zero : p = 0

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : p = 0
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_dvd (a b : R) : gcd a b ∣ a ∧ gcd a b ∣ b :=
  GCD.induction a b
    (fun b => by
      rw [gcd_zero_left]
      exact ⟨dvd_zero _, dvd_rfl⟩)
    fun a b _ ⟨IH₁, IH₂⟩ => by
    rw [gcd_val]
    exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ b ∣ 0 ∧ b ∣ b

Tactic:
exact ⟨dvd_zero _, dvd_rfl⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b

Tactic:
rw [gcd_zero_left]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ b ∣ 0 ∧ b ∣ b

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b

Tactic:
exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

Tactic:
rw [gcd_val]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_mul_aux {p q : R[X]} :
    GCDMonoid.gcd (p * q).eraseLead.content p.leadingCoeff =
      GCDMonoid.gcd (p.eraseLead * q).content p.leadingCoeff

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd p.leadingCoeff (p * q).eraseLead.content = gcd p.leadingCoeff (p.eraseLead * q).content

Tactic:
apply gcd_content_eq_of_dvd_sub

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q

Tactic:
rw [← self_sub_C_mul_X_pow, ← self_sub_C_mul_X_pow, sub_mul, sub_sub, add_comm, sub_add,
  sub_sub_cancel, leadingCoeff_mul, RingHom.map_mul, mul_assoc, mul_assoc]

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff

Tactic:
rw [gcd_comm (content _) _, gcd_comm (content _) _]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd p.leadingCoeff (p * q).eraseLead.content = gcd p.leadingCoeff (p.eraseLead * q).content

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)

Tactic:
apply dvd_sub (Dvd.intro _ rfl) (Dvd.intro _ rfl)

Result:
no goals
-- Mathlib/Data/Multiset/Basic.lean
theorem strongInductionOn_eq {p : Multiset α → Sort*} (s : Multiset α) (H) :
    @strongInductionOn _ p s H = H s fun t _h => @strongInductionOn _ p t H

Proof state:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ s.strongInductionOn H = H s fun t _h => t.strongInductionOn H

Tactic:
rw [strongInductionOn]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma inv_smul_finset_distrib (a : α) (s : Finset α) : (a • s)⁻¹ = op a⁻¹ • s⁻¹

Proof state:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (a • s)⁻¹ ↔ a✝ ∈ op a⁻¹ • s⁻¹

Proof state:
case h
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (a • s)⁻¹ ↔ a✝ ∈ op a⁻¹ • s⁻¹

Tactic:
simp [← inv_smul_mem_iff]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem injective_sym2 : Function.Injective (Finset.sym2 : Finset α → _)

Proof state:
α : Type u_1
⊢ Function.Injective Finset.sym2

Tactic:
intro s t h

Result:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
⊢ s = t

Proof state:
case h
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t

Tactic:
simpa using congr(s(x, x) ∈ $h)

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
⊢ s = t

Tactic:
ext x

Result:
case h
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t
-- Mathlib/Data/Complex/Trigonometric.lean
theorem inv_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) : (1 + tan x ^ 2)⁻¹ = cos x ^ 2

Proof state:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2

Tactic:
rw [tan_eq_sin_div_cos, div_pow]

Result:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2

Proof state:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2

Tactic:
field_simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv (h : S.LeftHomologyData) :
    h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom

Tactic:
dsimp only [homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.leftHomologyIso.hom ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = S.leftHomologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.leftHomologyIso.hom ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = S.leftHomologyIso.hom

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Tactic/Rify.lean
@[rify_simps] lemma ratCast_le (a b : ℚ) : a ≤ b ↔ (a : ℝ) ≤ (b : ℝ)

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

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    m.1.keys.contains k = m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ m.val.keys.contains k = m.contains k

Tactic:
simp_to_model using List.containsKey_eq_keys_contains.symm

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma measurable_density_left (κ : Kernel α (γ × β)) (ν : Kernel α γ) (x : γ)
    {s : Set β} (hs : MeasurableSet s) :
    Measurable (fun a ↦ density κ ν a x s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable ((fun p => κ.density ν p.1 p.2 s) ∘ fun a => (a, x))

Tactic:
exact (measurable_density κ ν hs).comp measurable_prod_mk_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => κ.density ν a x s

Tactic:
change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun a ↦ (a, x)))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable ((fun p => κ.density ν p.1 p.2 s) ∘ fun a => (a, x))
-- Mathlib/SetTheory/Game/PGame.lean
theorem Subsequent.moveRight_mk_right {xL : xl → PGame} {i : xr} (xR : xr → PGame) (j) :
    Subsequent ((xR i).moveRight j) (mk xl xr xL xR)

Proof state:
xl xr : Type u
xL : xl → PGame
i : xr
xR : xr → PGame
j : (xR i).RightMoves
⊢ ((xR i).moveRight j).Subsequent (mk xl xr xL xR)

Tactic:
pgame_wf_tac

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquiv_mk (x y) : algEquiv M S (mk x y) = mk' S x y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S) (mk x y) = mk' S x y

Tactic:
rw [mk_eq_mk', algEquiv_mk']

Result:
no goals
-- Mathlib/Analysis/Quaternion.lean
theorem hasSum_coe {f : α → ℝ} {r : ℝ} : HasSum (fun a => (f a : ℍ)) (↑r : ℍ) ↔ HasSum f r :=
  ⟨fun h => by
    simpa only using
    h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _ _) continuous_re,
    fun h => by simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)⟩

Proof state:
α : Type u_1
f : α → ℝ
r : ℝ
h : HasSum f r
⊢ HasSum (fun a => ↑(f a)) ↑r

Tactic:
simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
r : ℝ
h : HasSum (fun a => ↑(f a)) ↑r
⊢ HasSum f r

Tactic:
simpa only using
h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _ _) continuous_re

Result:
no goals
-- Mathlib/Order/Category/FinBddDistLat.lean
lemma inv_hom_apply {X Y : FinBddDistLat} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : FinBddDistLat
e : X ≅ Y
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem forall_zero_iff {P : BitVec 0 → Prop} :
    (∀ v, P v) ↔ P 0#0

Proof state:
P : BitVec 0 → Prop
⊢ (∀ (v : BitVec 0), P v) ↔ P 0#0

Tactic:
constructor

Result:
case mp
P : BitVec 0 → Prop
⊢ (∀ (v : BitVec 0), P v) → P 0#0

case mpr
P : BitVec 0 → Prop
⊢ P 0#0 → ∀ (v : BitVec 0), P v

Proof state:
case mpr
P : BitVec 0 → Prop
h : P 0#0
⊢ P 0#0

Tactic:
apply h

Result:
no goals

Proof state:
case mpr
P : BitVec 0 → Prop
⊢ P 0#0 → ∀ (v : BitVec 0), P v

Tactic:
intro h v

Result:
case mpr
P : BitVec 0 → Prop
h : P 0#0
v : BitVec 0
⊢ P v

Proof state:
case mp
P : BitVec 0 → Prop
⊢ (∀ (v : BitVec 0), P v) → P 0#0

Tactic:
intro h

Result:
case mp
P : BitVec 0 → Prop
h : ∀ (v : BitVec 0), P v
⊢ P 0#0

Proof state:
case mp
P : BitVec 0 → Prop
h : ∀ (v : BitVec 0), P v
⊢ P 0#0

Tactic:
apply h

Result:
no goals

Proof state:
case mpr
P : BitVec 0 → Prop
h : P 0#0
v : BitVec 0
⊢ P v

Tactic:
obtain (rfl : v = 0#0) := (by ext i ⟨⟩)

Result:
case mpr
P : BitVec 0 → Prop
h : P 0#0
⊢ P 0#0

Proof state:
P : BitVec 0 → Prop
h : P 0#0
v : BitVec 0
⊢ v = 0#0

Tactic:
ext i ⟨⟩

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem aeval_continuousMap_apply (g : R[X]) (f : C(α, R)) (x : α) :
    ((Polynomial.aeval f) g) x = g.eval (f x)

Proof state:
case refine_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
p q : R[X]
hp : ((aeval f) p) x = eval (f x) p
hq : ((aeval f) q) x = eval (f x) q
⊢ ((aeval f) (p + q)) x = eval (f x) (p + q)

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ((aeval f) g) x = eval (f x) g

Tactic:
refine Polynomial.induction_on' g ?_ ?_

Result:
case refine_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (p q : R[X]),
    ((aeval f) p) x = eval (f x) p → ((aeval f) q) x = eval (f x) q → ((aeval f) (p + q)) x = eval (f x) (p + q)

case refine_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (n : ℕ) (a : R), ((aeval f) ((monomial n) a)) x = eval (f x) ((monomial n) a)

Proof state:
case refine_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
n : ℕ
a : R
⊢ ((aeval f) ((monomial n) a)) x = eval (f x) ((monomial n) a)

Tactic:
simp [Pi.pow_apply]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (n : ℕ) (a : R), ((aeval f) ((monomial n) a)) x = eval (f x) ((monomial n) a)

Tactic:
intro n a

Result:
case refine_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
n : ℕ
a : R
⊢ ((aeval f) ((monomial n) a)) x = eval (f x) ((monomial n) a)

Proof state:
case refine_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (p q : R[X]),
    ((aeval f) p) x = eval (f x) p → ((aeval f) q) x = eval (f x) q → ((aeval f) (p + q)) x = eval (f x) (p + q)

Tactic:
intro p q hp hq

Result:
case refine_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
p q : R[X]
hp : ((aeval f) p) x = eval (f x) p
hq : ((aeval f) q) x = eval (f x) q
⊢ ((aeval f) (p + q)) x = eval (f x) (p + q)
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_injective : Injective ord

Proof state:
c c' : Cardinal.{u_1}
h : c.ord = c'.ord
⊢ c = c'

Tactic:
rw [← card_ord c, ← card_ord c', h]

Result:
no goals

Proof state:
⊢ Injective ord

Tactic:
intro c c' h

Result:
c c' : Cardinal.{u_1}
h : c.ord = c'.ord
⊢ c = c'
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem dvd_mul_gcd_iff_dvd_mul : x ∣ n * gcd x m ↔ x ∣ n * m

Proof state:
x n m : ℕ
⊢ x ∣ n * x.gcd m ↔ x ∣ n * m

Tactic:
rw [mul_comm, dvd_gcd_mul_iff_dvd_mul, mul_comm]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
    Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b

Proof state:
n : ℕ
hn : 0 < n
a b : ℕ
⊢ a.Coprime (b ^ n) ↔ a.Coprime b

Tactic:
rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]

Result:
no goals
-- Mathlib/Geometry/Manifold/AnalyticManifold.lean
/-- `f ∈ analyticGroupoid` iff it and its inverse are analytic within `range I`. -/
lemma mem_analyticGroupoid {I : ModelWithCorners 𝕜 E H} {f : PartialHomeomorph H H} :
    f ∈ analyticGroupoid I ↔
      AnalyticOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' f.source ∩ range I) ∧
      AnalyticOn 𝕜 (I ∘ f.symm ∘ I.symm) (I.symm ⁻¹' f.target ∩ range I)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
f : PartialHomeomorph H H
⊢ f ∈ analyticGroupoid I ↔
    AnalyticOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) ∧
      AnalyticOn 𝕜 (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem EventuallyEq.sub_eq [AddGroup β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
    f - g =ᶠ[l] 0

Proof state:
α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0

Tactic:
simpa using ((EventuallyEq.refl l f).sub h).symm

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive]
lemma prod_lt_one (hf : f < 1) : ∏ i, f i < 1 :=
  Finset.prod_lt_one' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : OrderedCancelCommMonoid M
f : ι → M
hf : f < 1
⊢ ∃ i ∈ Finset.univ, f i < 1

Tactic:
simpa using (Pi.lt_def.1 hf).2

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsClosed.exists_closed_singleton [T0Space X] [CompactSpace X] {S : Set X}
    (hS : IsClosed S) (hne : S.Nonempty) : ∃ x : X, x ∈ S ∧ IsClosed ({x} : Set X)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
⊢ ∃ x ∈ S, IsClosed {x}

Tactic:
obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
V : Set X
Vsub : V ⊆ S
Vne : V.Nonempty
Vcls : IsClosed V
hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V
⊢ ∃ x ∈ S, IsClosed {x}

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
x : X
Vsub : {x} ⊆ S
Vne : {x}.Nonempty
Vcls : IsClosed {x}
hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed V' → V' = {x}
⊢ ∃ x ∈ S, IsClosed {x}

Tactic:
exact ⟨x, Vsub (mem_singleton x), Vcls⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
V : Set X
Vsub : V ⊆ S
Vne : V.Nonempty
Vcls : IsClosed V
hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V
⊢ ∃ x ∈ S, IsClosed {x}

Tactic:
rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T0Space X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
x : X
Vsub : {x} ⊆ S
Vne : {x}.Nonempty
Vcls : IsClosed {x}
hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed V' → V' = {x}
⊢ ∃ x ∈ S, IsClosed {x}
-- Mathlib/Algebra/Order/Monovary.lean
lemma antivaryOn_inv₀ (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) :
    AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ i ∈ s, 0 < f i
hg : ∀ i ∈ s, 0 < g i
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Tactic:
rw [antivaryOn_inv_left₀ hf, monovaryOn_inv_right₀ hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.WF) {l : List α} {k : α} :
    k ∈ m → getKey? (insertManyIfNewUnit m l) k = getKey? m k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ k ∈ m → (insertManyIfNewUnit m l).getKey? k = m.getKey? k

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).getKey? k = m.getKey? k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).getKey? k = m.getKey? k

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_tail (l : List α) : (tail l).head? = l[1]?

Proof state:
α : Type u_1
l : List α
⊢ l.tail.head? = l[1]?

Tactic:
simp [head?_eq_getElem?]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem edist_efixedPoint_le (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞) :
    edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - K)

Proof state:
case h.e'_4.h.e'_5
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0

Tactic:
simp only [pow_zero, mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)

Tactic:
convert hf.apriori_edist_iterate_efixedPoint_le hx 0

Result:
case h.e'_4.h.e'_5
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_lt_univ (c : Cardinal) : lift.{u + 1, u} c < univ.{u, u + 1}

Proof state:
c : Cardinal.{u}
⊢ lift.{u + 1, u} c < univ.{u, u + 1}

Tactic:
simpa only [liftPrincipalSeg_coe, lift_ord, lift_succ, ord_le, succ_le_iff] using
  le_of_lt (liftPrincipalSeg.{u, u + 1}.lt_top (succ c).ord)

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS'_four : preNormEDS' b c d 4 = d

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS' b c d 4 = d

Tactic:
rw [preNormEDS']

Result:
no goals