harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_smul_measure (r : ℝ≥0∞) (f : α → ℝ≥0∞) :
    (r • μ).withDensity f = r • μ.withDensity f

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((r • μ).withDensity f) s = (r • μ.withDensity f) s

Tactic:
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
  smul_eq_mul, setLIntegral_smul_measure]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (r • μ).withDensity f = r • μ.withDensity f

Tactic:
ext s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((r • μ).withDensity f) s = (r • μ.withDensity f) s
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem pow_dvd_of_mul_eq_pow [GCDMonoid α] {a b c d₁ d₂ : α} (ha : a ≠ 0) (hab : IsUnit (gcd a b))
    {k : ℕ} (h : a * b = c ^ k) (hc : c = d₁ * d₂) (hd₁ : d₁ ∣ a) : d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k

Tactic:
exact mul_pow d₁ d₂ k

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
h4 : d₁ ^ k ≠ 0
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
exact ⟨h4, h3⟩

Result:
no goals

Proof state:
case hu.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b)

Tactic:
apply isUnit_of_dvd_one

Result:
case hu.a.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ∣ 1

Proof state:
case hu
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b ^ k)

Tactic:
apply IsUnit.pow

Result:
case hu.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
have h3 : d₁ ^ k ∣ a := by
  apply (dvd_gcd_mul_of_dvd_mul h2).trans
  rw [h1.mul_left_dvd]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem ContDiffAt.dist (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (hne : f x ≠ g x) :
    ContDiffAt ℝ n (fun y => dist (f y) (g y)) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => ‖f y - g y‖) x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => Dist.dist (f y) (g y)) x

Tactic:
simp only [dist_eq_norm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => ‖f y - g y‖) x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    {fallback : β k} {v : β k} : getValueCastD k (insertEntry k v l) fallback = v

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
fallback v : β k
⊢ getValueCastD k (insertEntry k v l) fallback = v

Tactic:
rw [getValueCastD_insertEntry, dif_pos BEq.refl, cast_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem inv_thickening : (thickening δ s)⁻¹ = thickening δ s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹

Tactic:
simp_rw [thickening, ← infEdist_inv]

Result:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}

Tactic:
rfl

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_eq_of_tendsto₀ {τ' : ℝ}
    (h : Tendsto (fun n : ℕ => f^[n] 0 / n) atTop (𝓝 τ')) : τ f = τ' :=
  f.translationNumber_eq_of_tendsto_aux <| by
    simpa [Function.comp_def, transnumAuxSeq_def, coe_pow] using
      h.comp (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two)

Proof state:
f : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n => (⇑f)^[n] 0 / ↑n) atTop (𝓝 τ')
⊢ Tendsto f.transnumAuxSeq atTop (𝓝 τ')

Tactic:
simpa [Function.comp_def, transnumAuxSeq_def, coe_pow] using
  h.comp (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two)

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem balanced_closedBall_zero (r : ℝ) : Balanced 𝕜 (closedBall p 0 r)

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun x => a • x) y = x
⊢ ‖a‖ * p y ≤ r

Tactic:
calc
  _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
  _ ≤ r := by rwa [mem_closedBall_zero] at hy

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun x => a • x) y = x
⊢ p y ≤ r

Tactic:
rwa [mem_closedBall_zero] at hy

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun x => a • x) y = x
⊢ x ∈ p.closedBall 0 r

Tactic:
rw [mem_closedBall_zero, ← hx, map_smul_eq_mul]

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun x => a • x) y = x
⊢ ‖a‖ * p y ≤ r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (p.closedBall 0 r)

Tactic:
rintro a ha x ⟨y, hy, hx⟩

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun x => a • x) y = x
⊢ x ∈ p.closedBall 0 r
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_le_self_iff : sinh x ≤ x ↔ x ≤ 0 :=
  calc
    sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0

Proof state:
x : ℝ
⊢ sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem take_append_of_le_length (h : n ≤ x.length) :
    (x ++ₛ a).take n = x.take n

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ ∀ (i : ℕ) (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    (take n (x ++ₛ a))[i] = (List.take n x)[i]

Tactic:
intro _ _ _

Result:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ take n (x ++ₛ a) = List.take n x

Tactic:
apply List.ext_getElem (by simp [h])

Result:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ ∀ (i : ℕ) (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    (take n (x ++ₛ a))[i] = (List.take n x)[i]

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ (take n (x ++ₛ a)).length = (List.take n x).length

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]

Tactic:
rw [List.getElem_take, take_get, get_append_left]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem coeff_toSubring {n : ℕ} : ↑(coeff (toSubring p T hp) n) = coeff p n

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

Tactic:
rw [h]

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ ↑((p.toSubring T hp).coeff n) = p.coeff n

Tactic:
simp only [toSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
  Ne, ite_not]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ ↑(if p.coeff n = 0 then 0 else ⟨p.coeff n, ⋯⟩) = p.coeff n

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ ↑(if p.coeff n = 0 then 0 else ⟨p.coeff n, ⋯⟩) = p.coeff n

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

case neg
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Proof state:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Tactic:
rfl

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_pos_iff (hx : 0 ≤ x) : 0 < log x ↔ 1 < x

Proof state:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 0 < log x ↔ 1 < x

Tactic:
rw [← log_one]

Result:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ 0 < log x ↔ 1 < x

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Result:
case inl
hx : 0 ≤ 0
⊢ 0 < log 0 ↔ 1 < 0

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 0 < log x ↔ 1 < x

Proof state:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x

Tactic:
exact log_lt_log_iff zero_lt_one hx

Result:
no goals

Proof state:
case inl
hx : 0 ≤ 0
⊢ 0 < log 0 ↔ 1 < 0

Tactic:
simp [le_refl, zero_le_one]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt (s : Set α) :
    s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard

Proof state:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < s.encard

Tactic:
rw [← encard_diff_singleton_add_one ha]

Result:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1

Proof state:
α : Type u_1
s : Set α
⊢ s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard

Tactic:
refine s.eq_empty_or_nonempty.elim Or.inl (Or.inr ∘ fun ⟨a,ha⟩ ↦
  (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, ?_⟩) (Or.inl ∘ Infinite.encard_eq)))

Result:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < s.encard

Proof state:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1

Tactic:
exact WithTop.add_lt_add_left hfin.diff.encard_lt_top.ne zero_lt_one

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1

Tactic:
nth_rw 1 [← add_zero (encard _)]

Result:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1
-- Mathlib/ModelTheory/Syntax.lean
theorem id_onTerm : ((LHom.id L).onTerm : L.Term α → L.Term α) = id

Proof state:
L : Language
α : Type u'
⊢ (LHom.id L).onTerm = id

Tactic:
ext t

Result:
case h
L : Language
α : Type u'
t : L.Term α
⊢ (LHom.id L).onTerm t = id t

Proof state:
case h
L : Language
α : Type u'
t : L.Term α
⊢ (LHom.id L).onTerm t = id t

Tactic:
induction t with
| var => rfl
| func _ _ ih => simp_rw [onTerm, ih]; rfl

Result:
no goals

Proof state:
case h.var
L : Language
α : Type u'
a✝ : α
⊢ (LHom.id L).onTerm (var a✝) = id (var a✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h.func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (func ((LHom.id L).onFunction _f✝) fun i => id (_ts✝ i)) = id (func _f✝ _ts✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h.func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (LHom.id L).onTerm (func _f✝ _ts✝) = id (func _f✝ _ts✝)

Tactic:
simp_rw [onTerm, ih]

Result:
case h.func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (func ((LHom.id L).onFunction _f✝) fun i => id (_ts✝ i)) = id (func _f✝ _ts✝)
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p z ≤ (p : ℚ) ^ (-n : ℤ)

Proof state:
case neg.hf
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ FiniteMultiplicity (↑p) z

Tactic:
apply Int.finiteMultiplicity_iff.2 ⟨by simp [hp.out.ne_one], mod_cast hz⟩

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ (↑p).natAbs ≠ 1

Tactic:
simp [hp.out.ne_one]

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

Tactic:
simp [hz]

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(multiplicity (↑p) z)

Tactic:
norm_cast

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ n ≤ multiplicity (↑p) z

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

Tactic:
exact_mod_cast hz

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
exact_mod_cast hp.out.one_lt

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ ↑p ^ (-↑n)

Tactic:
split_ifs with hz

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

Tactic:
norm_cast at hz

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ n ∣ z

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)

Tactic:
unfold padicNorm

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ ↑p ^ (-↑n)

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ n ≤ multiplicity (↑p) z

Tactic:
rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ n ∣ z

case neg.hf
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ FiniteMultiplicity (↑p) z

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)

Tactic:
rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
  padicValInt.of_ne_one_ne_zero hp.1.ne_one _]

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(multiplicity (↑p) z)

p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
-- Mathlib/NumberTheory/ClassNumber/Finite.lean
theorem normBound_pos : 0 < normBound abv bS

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 <
    (↑(Fintype.card ι) *
        (Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^
      Fintype.card ι

Tactic:
refine pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) ?_) _

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 < (Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
⊢ 0 < normBound abv bS

Tactic:
obtain ⟨i, j, k, hijk⟩ : ∃ i j k, Algebra.leftMulMatrix bS (bS i) j k ≠ 0 := by
  by_contra! h
  obtain ⟨i⟩ := bS.index_nonempty
  apply bS.ne_zero i
  apply
    (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
  ext j k
  simp [h, DMatrix.zero_apply]

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 < normBound abv bS
-- Mathlib/Data/Finsupp/Single.lean
theorem update_self : f.update a (f a) = f

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.update a (f a) = f

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a a✝ : α
⊢ (f.update a (f a)) a✝ = f a✝

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a a✝ : α
⊢ (f.update a (f a)) a✝ = f a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.update a (f a) = f

Tactic:
classical
  ext
  simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
/-- A version of `Matroid.spanning_iff_exists_isBase_subset` in which the `S ⊆ M.E` condition
appears in the RHS of the equivalence rather than as a hypothesis. -/
lemma spanning_iff_exists_isBase_subset' : M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Proof state:
case intro
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
have hB' := hB.isBasis_closure_right

Result:
case intro
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B (M.closure S)
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Proof state:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBasis S

Result:
case intro
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Proof state:
case intro
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B (M.closure S)
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
rw [h.closure_eq, isBasis_ground_iff] at hB'

Result:
case intro
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Proof state:
case intro
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
exact ⟨B, hB', hB.subset⟩

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
S : Set α
⊢ M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩

Result:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_neg_apply {e : ℝ≥0} (he : e ≠ 0) {x : ℤₘ₀} (hx : x ≠ 0) :
    toNNReal he x = e ^ (WithZero.unzero hx).toAdd

Proof state:
case neg
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
h✝ : ¬x = 0
⊢ e ^ toAdd (unzero h✝) = e ^ toAdd (unzero hx)

Tactic:
rfl

Result:
no goals

Proof state:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
⊢ (toNNReal he) x = e ^ toAdd (unzero hx)

Tactic:
simp only [toNNReal, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
⊢ (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) = e ^ toAdd (unzero hx)

Proof state:
case pos
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
h✝ : x = 0
⊢ 0 = e ^ toAdd (unzero hx)

Tactic:
tauto

Result:
no goals

Proof state:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
⊢ (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) = e ^ toAdd (unzero hx)

Tactic:
split_ifs

Result:
case pos
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
h✝ : x = 0
⊢ 0 = e ^ toAdd (unzero hx)

case neg
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x ≠ 0
h✝ : ¬x = 0
⊢ e ^ toAdd (unzero h✝) = e ^ toAdd (unzero hx)
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem const_fac_thru_zero (n m : SimplexCategory) (i : Fin (m.len + 1)) :
    const n m i = const n ⦋0⦌ 0 ≫ SimplexCategory.const ⦋0⦌ m i

Proof state:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i)) 0)

Tactic:
rfl

Result:
no goals

Proof state:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const ⦋0⦌ 0 ≫ ⦋0⦌.const m i

Tactic:
rw [const_comp]

Result:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i)) 0)