harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_Ψ₃ : (W.map f).Ψ₃ = W.Ψ₃.map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).Ψ₃ = Polynomial.map f W.Ψ₃

Tactic:
simp only [Ψ₃, map_b₂, map_b₄, map_b₆, map_b₈]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ 3 * X ^ 4 + C (f W.b₂) * X ^ 3 + 3 * C (f W.b₄) * X ^ 2 + 3 * C (f W.b₆) * X + C (f W.b₈) =
    Polynomial.map f (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ 3 * X ^ 4 + C (f W.b₂) * X ^ 3 + 3 * C (f W.b₄) * X ^ 2 + 3 * C (f W.b₆) * X + C (f W.b₈) =
    Polynomial.map f (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_ite_zero : (∏ i, if p i then f i else 0) = if ∀ i, p i then ∏ i, f i else 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : Fintype ι
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
⊢ (∏ i : ι, if p i then f i else 0) = if ∀ (i : ι), p i then ∏ i : ι, f i else 0

Tactic:
simp [Finset.prod_ite_zero]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
/-- If `‖v‖^n * ‖f v‖` is integrable for all `n ≤ N`, then the `n`-th derivative of the Fourier
transform of `f` is the Fourier transform of `fourierPowSMulRight L f v n`,
i.e., `(L v ⬝) ^ n • f v`. -/
lemma iteratedFDeriv_fourierIntegral {N : ℕ∞}
    (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖^n * ‖f v‖) μ)
    (h'f : AEStronglyMeasurable f μ) {n : ℕ} (hn : n ≤ N) :
    iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₂ f) =
      fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v ↦ fourierPowSMulRight L f v n)

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
⊢ iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₂ f) =
    fourierIntegral 𝐞 μ L.toLinearMap₂ fun v => fourierPowSMulRight L f v n

Tactic:
ext w : 1

Result:
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
w : W
⊢ iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w =
    fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) w

Proof state:
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
w : W
⊢ iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w =
    fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) w

Tactic:
exact ((hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f).eq_iteratedFDeriv
  (mod_cast hn) w).symm

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem ae_empty_or_univ_of_image_ae_le' (hf : Ergodic f μ) (hs : NullMeasurableSet s μ)
    (hs' : f '' s ≤ᵐ[μ] s) (h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f '' s ≤ᶠ[ae μ] s
h_fin : μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
  (HasSubset.Subset.eventuallyLE (subset_preimage_image f s)).trans
    (hf.quasiMeasurePreserving.preimage_mono_ae hs')

Result:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
h_fin : μ s ≠ ⊤
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
h_fin : μ s ≠ ⊤
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
lemma Subring.mem_closure_image_of {S T : Type*} [CommRing S] [CommRing T] (g : S →+* T)
    (u : Set S) (x : S) (hx : x ∈ Subring.closure u) : g x ∈ Subring.closure (g '' u)

Proof state:
case a
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ ⇑g '' u ⊆ ↑T₁

Tactic:
exact h₁

Result:
no goals

Proof state:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ g x ∈ T₁

Tactic:
rw [← Subring.mem_comap]

Result:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ x ∈ Subring.comap g T₁

Proof state:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : x ∈ Subring.closure u
⊢ g x ∈ Subring.closure (⇑g '' u)

Tactic:
rw [Subring.mem_closure] at hx ⊢

Result:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
⊢ ∀ (S_1 : Subring T), ⇑g '' u ⊆ ↑S_1 → g x ∈ S_1

Proof state:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ x ∈ Subring.comap g T₁

Tactic:
apply hx

Result:
case a
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ u ⊆ ↑(Subring.comap g T₁)

Proof state:
case a
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ u ⊆ ↑(Subring.comap g T₁)

Tactic:
simp only [Subring.coe_comap, ← Set.image_subset_iff, SetLike.mem_coe]

Result:
case a
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ ⇑g '' u ⊆ ↑T₁

Proof state:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
⊢ ∀ (S_1 : Subring T), ⇑g '' u ⊆ ↑S_1 → g x ∈ S_1

Tactic:
intro T₁ h₁

Result:
S : Type u_1
T : Type u_2
inst✝¹ : CommRing S
inst✝ : CommRing T
g : S →+* T
u : Set S
x : S
hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1
T₁ : Subring T
h₁ : ⇑g '' u ⊆ ↑T₁
⊢ g x ∈ T₁
-- Mathlib/Order/Defs/LinearOrder.lean
lemma max_left_comm (a b c : α) : max a (max b c) = max b (max a c)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ max a (max b c) = max b (max a c)

Tactic:
rw [← max_assoc, max_comm a, max_assoc]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma map_neg_eq_conj [AddCommGroup G] (ψ : AddChar G K) (x : G) : ψ (-x) = conj (ψ x)

Proof state:
K : Type u_1
inst✝² : RCLike K
G : Type u_3
inst✝¹ : Finite G
inst✝ : AddCommGroup G
ψ : AddChar G K
x : G
⊢ ψ (-x) = (starRingEnd K) (ψ x)

Tactic:
rw [map_neg_eq_inv, inv_apply_eq_conj]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_add_eq_tsub_left (a b c : α) : a + b - (a + c) = b - c

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

Tactic:
rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
lemma exp_sub_sum_range_isBigO_pow (n : ℕ) :
    (fun x ↦ exp x - ∑ i ∈ Finset.range n, x ^ i / i !) =O[𝓝 0] (· ^ n)

Proof state:
case h.e'_4
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖ = ‖x‖ ^ n * (↑n.succ * (↑n ! * ↑n)⁻¹)

Tactic:
field_simp [mul_comm]

Result:
no goals

Proof state:
case inr
n : ℕ
hn : 0 < n
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Tactic:
rw [NormedAddCommGroup.nhds_zero_basis_norm_lt.eventually_iff]

Result:
case inr
n : ℕ
hn : 0 < n
⊢ ∃ i,
    0 < i ∧
      ∀ ⦃x : ℂ⦄, x ∈ {y | ‖y‖ < i} → ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Proof state:
case inr
n : ℕ
hn : 0 < n
⊢ (fun x => cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Tactic:
refine .of_bound (n.succ / (n ! * n)) ?_

Result:
case inr
n : ℕ
hn : 0 < n
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Proof state:
case inl

⊢ (fun x => cexp x - ∑ i ∈ Finset.range 0, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ 0

Tactic:
simpa using continuous_exp.continuousAt.norm.isBoundedUnder_le

Result:
no goals

Proof state:
case inr
n : ℕ
hn : 0 < n
⊢ ∃ i,
    0 < i ∧
      ∀ ⦃x : ℂ⦄, x ∈ {y | ‖y‖ < i} → ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Tactic:
refine ⟨1, one_pos, fun x hx ↦ ?_⟩

Result:
case inr
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Proof state:
n : ℕ
⊢ (fun x => cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Tactic:
rcases (zero_le n).eq_or_lt with rfl | hn

Result:
case inl

⊢ (fun x => cexp x - ∑ i ∈ Finset.range 0, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ 0

case inr
n : ℕ
hn : 0 < n
⊢ (fun x => cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n

Proof state:
case inr
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Tactic:
convert exp_bound hx.out.le hn using 1

Result:
case h.e'_4
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖ = ‖x‖ ^ n * (↑n.succ * (↑n ! * ↑n)⁻¹)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_map (f : β → γ) (l : Vector β n) : findSome? p (l.map f) = l.findSome? (p ∘ f)

Proof state:
β : Type u_1
γ : Type u_2
n : Nat
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
l : Vector β n
⊢ findSome? p (map f l) = findSome? (p ∘ f) l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
l : Array β
⊢ findSome? p (map f { toArray := l, size_toArray := ⋯ }) = findSome? (p ∘ f) { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
l : Array β
⊢ findSome? p (map f { toArray := l, size_toArray := ⋯ }) = findSome? (p ∘ f) { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.findSome?_map]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem image_bot (s : Set α) : (⊥ : Rel α β).image s = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
⊢ ∀ (x : β), x ∉ ⊥.image s

Tactic:
intro x h

Result:
α : Type u_1
β : Type u_2
s : Set α
x : β
h : x ∈ ⊥.image s
⊢ False

Proof state:
α : Type u_1
β : Type u_2
s : Set α
⊢ ⊥.image s = ∅

Tactic:
rw [Set.eq_empty_iff_forall_not_mem]

Result:
α : Type u_1
β : Type u_2
s : Set α
⊢ ∀ (x : β), x ∉ ⊥.image s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
x : β
h : x ∈ ⊥.image s
⊢ False

Tactic:
simp [mem_image, Bot.bot] at h

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 < r) :
    ball (s.sup p) x r = s.inf fun i => ball (p i) x r

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = s.inf fun i => (p i).ball x r

Tactic:
rw [Finset.inf_eq_iInf]

Result:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r

Tactic:
exact ball_finset_sup_eq_iInter _ _ _ hr

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharNeTwoNF : W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Tactic:
rw [b₈, a₁_of_isCharNeTwoNF, a₃_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 0 * 0 * W.a₄ + W.a₂ * 0 ^ 2 - W.a₄ ^ 2 = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 0 * 0 * W.a₄ + W.a₂ * 0 ^ 2 - W.a₄ ^ 2 = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem im_le_im_mul_exp_dist (z w : ℍ) : z.im ≤ w.im * Real.exp (dist z w)

Proof state:
z w : ℍ
⊢ z.im ≤ w.im * rexp (dist z w)

Tactic:
rw [← div_le_iff₀' w.im_pos, ← exp_log z.im_pos, ← exp_log w.im_pos, ← Real.exp_sub, exp_le_exp]

Result:
z w : ℍ
⊢ log z.im - log w.im ≤ dist z w

Proof state:
z w : ℍ
⊢ log z.im - log w.im ≤ dist z w

Tactic:
exact (le_abs_self _).trans (dist_log_im_le z w)

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
lemma natCast_le_rank_iff_finset [Nontrivial R] {n : ℕ} :
    n ≤ Module.rank R M ↔ ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) :=
  ⟨exists_finset_linearIndependent_of_le_rank,
    fun ⟨s, h₁, h₂⟩ ↦ by simpa [h₁] using h₂.cardinal_le_rank⟩

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ s, s.card = n ∧ LinearIndependent R Subtype.val
s : Finset M
h₁ : s.card = n
h₂ : LinearIndependent R Subtype.val
⊢ ↑n ≤ Module.rank R M

Tactic:
simpa [h₁] using h₂.cardinal_le_rank

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem restrict_apply (μ : FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) :
    (μ.restrict A) s = μ (s ∩ A)

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ ↑(μ.restrict A) s = ↑μ (s ∩ A)

Tactic:
exact Measure.restrict_apply s_mble

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ (μ.restrict A) s = μ (s ∩ A)

Tactic:
apply congr_arg ENNReal.toNNReal

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ ↑(μ.restrict A) s = ↑μ (s ∩ A)
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_lsub_le_lift {ι} (f : ι → Ordinal) :
    cof (lsub.{u, v} f) ≤ Cardinal.lift.{v, u} #ι

Proof state:
case h.e'_3.h.e'_1
ι : Type u
f : ι → Ordinal.{max u v}
⊢ lsub f = lsub fun i => f i.down

Tactic:
exact
  lsub_eq_of_range_eq.{u, max u v, max u v}
    (Set.ext fun x => ⟨fun ⟨i, hi⟩ => ⟨ULift.up.{v, u} i, hi⟩, fun ⟨i, hi⟩ => ⟨_, hi⟩⟩)

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lsub f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← mk_uLift.{u, v}]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lsub f).cof ≤ #(ULift.{v, u} ι)

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lsub f).cof ≤ #(ULift.{v, u} ι)

Tactic:
convert cof_lsub_le.{max u v} fun i : ULift.{v, u} ι => f i.down

Result:
case h.e'_3.h.e'_1
ι : Type u
f : ι → Ordinal.{max u v}
⊢ lsub f = lsub fun i => f i.down
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- There exists an automorphism `f` of `A` that maps `b` to `a`.
`f` is obtained by considering `u` and `selfProdPermIncl h b`.
Both are inclusions of `A` into `selfProd F X` mapping `b` respectively `a` to the same element
in the fiber of `selfProd F X`. Applying `connected_component_unique` yields the result. -/
private lemma subobj_selfProd_trans [Mono u] (b : F.obj A) : ∃ (f : A ≅ A), F.map f.hom b = a

Proof state:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝² : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝¹ : IsConnected A
inst✝ : Mono u
b : (F.obj A).carrier
⊢ ∃ f, F.map f.hom b = a

Tactic:
apply connected_component_unique F b a u (selfProdPermIncl h b)

Result:
case h
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝² : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝¹ : IsConnected A
inst✝ : Mono u
b : (F.obj A).carrier
⊢ F.map u b = F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a

Proof state:
case h
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝² : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝¹ : IsConnected A
inst✝ : Mono u
b : (F.obj A).carrier
⊢ F.map u b = F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a

Tactic:
exact selfProdTermIncl_fib_eq h b

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem singleton_sigma : ({i} : Set ι).sigma t = Sigma.mk i '' t i :=
  ext fun x ↦ by
    constructor
    · obtain ⟨j, a⟩ := x
      rintro ⟨rfl : j = i, ha⟩
      exact mem_image_of_mem _ ha
    · rintro ⟨b, hb, rfl⟩
      exact ⟨rfl, hb⟩

Proof state:
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
x : (i : ι) × α i
⊢ x ∈ {i}.sigma t ↔ x ∈ Sigma.mk i '' t i

Tactic:
constructor

Result:
case mp
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
x : (i : ι) × α i
⊢ x ∈ {i}.sigma t → x ∈ Sigma.mk i '' t i

case mpr
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
x : (i : ι) × α i
⊢ x ∈ Sigma.mk i '' t i → x ∈ {i}.sigma t

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
x : (i : ι) × α i
⊢ x ∈ Sigma.mk i '' t i → x ∈ {i}.sigma t

Tactic:
rintro ⟨b, hb, rfl⟩

Result:
case mpr.intro.intro
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
b : α i
hb : b ∈ t i
⊢ ⟨i, b⟩ ∈ {i}.sigma t

Proof state:
case mp.mk
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i j : ι
a : α j
⊢ ⟨j, a⟩ ∈ {i}.sigma t → ⟨j, a⟩ ∈ Sigma.mk i '' t i

Tactic:
rintro ⟨rfl : j = i, ha⟩

Result:
case mp.mk.intro
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
j : ι
a : α j
ha : ⟨j, a⟩.snd ∈ t ⟨j, a⟩.fst
⊢ ⟨j, a⟩ ∈ Sigma.mk j '' t j

Proof state:
case mp
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
x : (i : ι) × α i
⊢ x ∈ {i}.sigma t → x ∈ Sigma.mk i '' t i

Tactic:
obtain ⟨j, a⟩ := x

Result:
case mp.mk
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i j : ι
a : α j
⊢ ⟨j, a⟩ ∈ {i}.sigma t → ⟨j, a⟩ ∈ Sigma.mk i '' t i

Proof state:
case mpr.intro.intro
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
b : α i
hb : b ∈ t i
⊢ ⟨i, b⟩ ∈ {i}.sigma t

Tactic:
exact ⟨rfl, hb⟩

Result:
no goals

Proof state:
case mp.mk.intro
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
j : ι
a : α j
ha : ⟨j, a⟩.snd ∈ t ⟨j, a⟩.fst
⊢ ⟨j, a⟩ ∈ Sigma.mk j '' t j

Tactic:
exact mem_image_of_mem _ ha

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite_self (n : ℕ) : coeff (hermite n) n = 1

Proof state:
n : ℕ
⊢ (hermite n).coeff n = 1

Tactic:
induction n with
| zero => exact coeff_C
| succ n ih =>
  rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
  simp

Result:
no goals

Proof state:
case zero

⊢ (hermite 0).coeff 0 = 1

Tactic:
exact coeff_C

Result:
no goals

Proof state:
case succ
n : ℕ
ih : (hermite n).coeff n = 1
⊢ n < n + 2

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
ih : (hermite n).coeff n = 1
⊢ (hermite (n + 1)).coeff (n + 1) = 1

Tactic:
rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]

Result:
case succ
n : ℕ
ih : (hermite n).coeff n = 1
⊢ n < n + 2
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_sSup_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    (s : Set β) : l (sSup (u '' s)) = sSup s

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sSup (u '' s)) = sSup s

Tactic:
rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_option_elim (a : α) (f : β → α) : ⨆ o : Option β, o.elim a f = a ⊔ ⨆ b, f b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
f : β → α
⊢ ⨆ o, o.elim a f = a ⊔ ⨆ b, f b

Tactic:
simp [iSup_option]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Integers.lean
lemma valuation_unit (hv : Integers v O) (x : Oˣ) :
    v (algebraMap O F x) = 1

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : Oˣ
⊢ v ((algebraMap O F) ↑x) = 1

Tactic:
simp [← hv.isUnit_iff_valuation_eq_one]

Result:
no goals