harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem sinh_half_dist_add_dist (a b c : ℍ) : sinh ((dist a b + dist b c) / 2) =
    (dist (a : ℂ) b * dist (c : ℂ) (conj ↑b) + dist (b : ℂ) c * dist (a : ℂ) (conj ↑b)) /
      (2 * √(a.im * c.im) * dist (b : ℂ) (conj ↑b))

Proof state:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * b.im) * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * c.im) * b.im))

Tactic:
congr 2

Result:
case e_a.e_a
a b c : ℍ
⊢ √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im

Proof state:
a b c : ℍ
⊢ sinh ((dist a b + dist b c) / 2) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Tactic:
simp only [add_div _ _ (2 : ℝ), sinh_add, sinh_half_dist, cosh_half_dist, div_mul_div_comm]

Result:
a b c : ℍ
⊢ dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) +
      dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Proof state:
case e_a.e_a
a b c : ℍ
⊢ √(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im

Tactic:
rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt,
    mul_comm] <;> exact (im_pos _).le

Result:
no goals

Proof state:
a b c : ℍ
⊢ dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) +
      dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Tactic:
rw [← add_div, Complex.dist_self_conj, coe_im, abs_of_pos b.im_pos, mul_comm (dist (b : ℂ) _),
  dist_comm (b : ℂ), Complex.dist_conj_comm, mul_mul_mul_comm, mul_mul_mul_comm _ _ _ b.im]

Result:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * b.im) * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * c.im) * b.im))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
    any n f = (List.finRange n).any (fun ⟨i, h⟩ => f i h)

Proof state:
case zero
f : (i : Nat) → i < 0 → Bool
⊢ any 0 f =
    (List.finRange 0).any fun x =>
      match x with
      | ⟨i, h⟩ => f i h

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
f : (i : Nat) → i < n → Bool
⊢ n.any f =
    (List.finRange n).any fun x =>
      match x with
      | ⟨i, h⟩ => f i h

Tactic:
induction n with
| zero => simp
| succ n ih => simp [ih, List.finRange_succ_last, List.any_map, Function.comp_def]

Result:
no goals

Proof state:
case succ
n : Nat
ih :
  ∀ (f : (i : Nat) → i < n → Bool),
    n.any f =
      (List.finRange n).any fun x =>
        match x with
        | ⟨i, h⟩ => f i h
f : (i : Nat) → i < n + 1 → Bool
⊢ (n + 1).any f =
    (List.finRange (n + 1)).any fun x =>
      match x with
      | ⟨i, h⟩ => f i h

Tactic:
simp [ih, List.finRange_succ_last, List.any_map, Function.comp_def]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Injective.lean
lemma _root_.RingHom.injective_stableUnderComposition :
    RingHom.StableUnderComposition (fun f ↦ Function.Injective f)

Proof state:
⊢ RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => Function.Injective ⇑f

Tactic:
intro R S T _ _ _ f g hf hg

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(g.comp f)

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective (⇑g ∘ ⇑f)

Tactic:
exact Function.Injective.comp hg hf

Result:
no goals

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(g.comp f)

Tactic:
simp only [RingHom.coe_comp]

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective (⇑g ∘ ⇑f)
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹ :=
  inv_eq_left_inv (by simp [h, smul_smul])

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
k : αˣ
h : IsUnit A.det
⊢ k⁻¹ • A⁻¹ * k • A = 1

Tactic:
simp [h, smul_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
theorem coe_ofSurjective (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) :
    ⇑(LinearIsometryEquiv.ofSurjective f hfr) = f

Proof state:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E₂
inst✝² : Module R₂ E₂
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ⇑f
⊢ ⇑(ofSurjective f hfr) = ⇑f

Tactic:
ext

Result:
case h
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E₂
inst✝² : Module R₂ E₂
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ⇑f
x✝ : F
⊢ (ofSurjective f hfr) x✝ = f x✝

Proof state:
case h
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E₂
inst✝² : Module R₂ E₂
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ⇑f
x✝ : F
⊢ (ofSurjective f hfr) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/DMatrix.lean
theorem map_map {M : DMatrix m n α} {β : m → n → Type w} {γ : m → n → Type z}
    {f : ∀ ⦃i j⦄, α i j → β i j} {g : ∀ ⦃i j⦄, β i j → γ i j} :
    (M.map f).map g = M.map fun _ _ x => g (f x)

Proof state:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (fun x x_1 x_2 => g (f x_2)) i✝ j✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
⊢ (M.map f).map g = M.map fun x x_1 x_2 => g (f x_2)

Tactic:
ext

Result:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (fun x x_1 x_2 => g (f x_2)) i✝ j✝
-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem lintegral_eq_lintegral_meas_lt (μ : Measure α)
    (f_nn : 0 ≤ᵐ[μ] f) (f_mble : AEMeasurable f μ) :
    ∫⁻ ω, ENNReal.ofReal (f ω) ∂μ = ∫⁻ t in Ioi 0, μ {a : α | t < f a}

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}

Tactic:
apply lintegral_congr_ae

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ (fun a => μ {a_1 | a ≤ f a_1}) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => μ {a_1 | a < f a_1}

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ (fun a => μ {a_1 | a ≤ f a_1}) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => μ {a_1 | a < f a_1}

Tactic:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
  with t ht

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ μ {a | t ≤ f a} = μ {a | t < f a}

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ μ {a | t ≤ f a} = μ {a | t < f a}

Tactic:
rw [ht]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}

Tactic:
rw [lintegral_eq_lintegral_meas_le μ f_nn f_mble]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
    {fallback : β a} (hl : DistinctKeys l) (h : Perm l l') :
    getValueCastD a l fallback = getValueCastD a l' fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
fallback : β a
hl : DistinctKeys l
h : l.Perm l'
⊢ getValueCastD a l fallback = getValueCastD a l' fallback

Tactic:
simp only [getValueCastD_eq_getValueCast?, getValueCast?_of_perm hl h]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma sum_apply_eq_zero_iff_ne_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Tactic:
classical
cases nonempty_fintype α
rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Proof state:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ ↑(Fintype.card α) ≠ 0

Tactic:
exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Tactic:
rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]

Result:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ ↑(Fintype.card α) ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_inj :
    ∀ {s₁ s₂ t₁ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → length s₁ = length s₂ → s₁ = s₂ ∧ t₁ = t₂
  | [], [], _, _, h, _ => ⟨rfl, h⟩
  | _ :: _, _ :: _, _, _, h, hl => by
    simp [append_inj (cons.inj h).2 (Nat.succ.inj hl)] at h ⊢; exact h

Proof state:
α : Type u_1
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ x✝¹ x✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
h : head✝¹ = head✝
⊢ head✝¹ = head✝

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ x✝¹ x✝ : List α
h : head✝¹ :: tail✝¹ ++ x✝¹ = head✝ :: tail✝ ++ x✝
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ x✝¹ = x✝

Tactic:
simp [append_inj (cons.inj h).2 (Nat.succ.inj hl)] at h ⊢

Result:
α : Type u_1
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ x✝¹ x✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
h : head✝¹ = head✝
⊢ head✝¹ = head✝
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem deg_pos [Nontrivial S] (h : IsAdjoinRootMonic S f) : 0 < natDegree f

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
⊢ 0 < f.natDegree

Tactic:
rcases h.basis.index_nonempty with ⟨⟨i, hi⟩⟩

Result:
case intro.mk
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
i : ℕ
hi : i < f.natDegree
⊢ 0 < f.natDegree

Proof state:
case intro.mk
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
i : ℕ
hi : i < f.natDegree
⊢ 0 < f.natDegree

Tactic:
exact (Nat.zero_le _).trans_lt hi

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma top_sub {x : EReal} (hx : x ≠ ⊤) : ⊤ - x = ⊤

Proof state:
x : EReal
hx : x ≠ ⊤
⊢ ⊤ - x = ⊤

Tactic:
cases x <;> tauto

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem sigma_eq_biUnion [DecidableEq (Σi, α i)] (s : Finset ι) (t : ∀ i, Finset (α i)) :
    s.sigma t = s.biUnion fun i => (t i).map <| Embedding.sigmaMk i

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma t = s.biUnion fun i => map (Embedding.sigmaMk i) (t i)

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ s.sigma t ↔ ⟨x, y⟩ ∈ s.biUnion fun i => map (Embedding.sigmaMk i) (t i)

Proof state:
case h.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ s.sigma t ↔ ⟨x, y⟩ ∈ s.biUnion fun i => map (Embedding.sigmaMk i) (t i)

Tactic:
simp [and_left_comm]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem exists_isOpen_mem_isCompact_closure (x : X) :
    ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
x : X
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

Tactic:
simpa only [singleton_subset_iff]
  using exists_isOpen_superset_and_isCompact_closure isCompact_singleton

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_pos_iff_support {f : α → ℝ≥0∞} (hf : Measurable f) :
    (0 < ∫⁻ a, f a ∂μ) ↔ 0 < μ (Function.support f)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ 0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (support f)

Tactic:
simp [pos_iff_ne_zero, hf, Filter.EventuallyEq, ae_iff, Function.support]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_three_mul : sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℝ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)

Proof state:
x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)

Tactic:
simp [sinh_three_mul]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsion_iff_isTorsion_int [AddCommGroup M] :
    AddMonoid.IsTorsion M ↔ Module.IsTorsion ℤ M

Proof state:
case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0

Tactic:
obtain ⟨n, hn⟩ := @h x

Result:
case refine_2.intro
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
n : ↥ℤ⁰
hn : n • x = 0
⊢ ∃ n, 0 < n ∧ n • x = 0

Proof state:
M : Type u_2
inst✝ : AddCommGroup M
⊢ IsTorsion M ↔ Module.IsTorsion ℤ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩

Result:
case refine_1
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion M
x : M
⊢ ∃ a, a • x = 0

case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ IsOfFinAddOrder x

Proof state:
case refine_2.intro
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
n : ↥ℤ⁰
hn : n • x = 0
⊢ ∃ n, 0 < n ∧ n • x = 0

Tactic:
exact ⟨_, Int.natAbs_pos.2 (nonZeroDivisors.coe_ne_zero n), natAbs_nsmul_eq_zero.2 hn⟩

Result:
no goals

Proof state:
case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ IsOfFinAddOrder x

Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]

Result:
case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0

Proof state:
case refine_1
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion M
x : M
⊢ ∃ a, a • x = 0

Tactic:
obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero

Result:
case refine_1.intro.intro
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0

Proof state:
case refine_1.intro.intro
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0

Tactic:
exact
  ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.natCast_pos.mpr h0⟩,
    (natCast_zsmul _ _).trans hn⟩

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_lt_ceil_of_lt_of_pos {a b : α} (h : a < b) (h' : 0 < b) : ⌊a⌋₊ < ⌈b⌉₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rcases le_or_lt 0 a with (ha | ha)

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊

case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ a < ↑⌈b⌉₊

Tactic:
exact h.trans_le (le_ceil _)

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rw [floor_lt ha]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ a < ↑⌈b⌉₊
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma minpolyDiv_eq_zero (hx : ¬IsIntegral R x) : minpolyDiv R x = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ¬IsIntegral R x
⊢ map (algebraMap R S)
        (if hx : IsIntegral R x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap R S) x x_1 = 0) hx else 0) /ₘ
      (X - C x) =
    0

Tactic:
rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ¬IsIntegral R x
⊢ minpolyDiv R x = 0

Tactic:
delta minpolyDiv minpoly

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ¬IsIntegral R x
⊢ map (algebraMap R S)
        (if hx : IsIntegral R x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap R S) x x_1 = 0) hx else 0) /ₘ
      (X - C x) =
    0
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_one_fst_of_isMulTwoCocycle {f : G × G → M} (hf : IsMulTwoCocycle f) (g : G) :
    f (1, g) = f (1, 1)

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
simpa only [one_smul, one_mul, mul_one, mul_right_inj] using (hf 1 1 g).symm

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma tendsto_toReal_atTop : Tendsto EReal.toReal (𝓝[≠] ⊤) atTop

Proof state:
⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop

Tactic:
exact tendsto_id

Result:
no goals

Proof state:
⊢ Tendsto toReal (𝓝[≠] ⊤) atTop

Tactic:
rw [nhdsWithin_top, tendsto_map'_iff]

Result:
⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop
-- Mathlib/LinearAlgebra/Orientation.lean
theorem map_eq_iff_det_pos [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M)
    (h : Fintype.card ι = finrank R M) :
    Orientation.map ι f x = x ↔ 0 < LinearMap.det (f : M →ₗ[R] M)

Proof state:
case inl
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Tactic:
have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero

Result:
case inl
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
H : finrank R M = 0
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Proof state:
case inr
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Tactic:
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

case inr
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Proof state:
case inl
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
H : finrank R M = 0
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Tactic:
simp [LinearMap.det_eq_one_of_finrank_eq_zero H]

Result:
no goals