harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Radical.lean
theorem divRadical_dvd_wronskian_left (a b : k[X]) : divRadical a ∣ wronskian a b

Proof state:
case h₂
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ derivative a * b

Tactic:
apply dvd_mul_of_dvd_left

Result:
case h₂.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ derivative a

Proof state:
case h₁
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a * derivative b

Tactic:
apply dvd_mul_of_dvd_left

Result:
case h₁.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a * derivative b - derivative a * b

Tactic:
apply dvd_sub

Result:
case h₁
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a * derivative b

case h₂
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ derivative a * b

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a.wronskian b

Tactic:
rw [wronskian]

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a * derivative b - derivative a * b

Proof state:
case h₁.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a

Tactic:
exact divRadical_dvd_self a

Result:
no goals

Proof state:
case h₂.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ derivative a

Tactic:
exact divRadical_dvd_derivative a

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem sum_range_measure_preimage_singleton (f : α →ₛ β) (μ : Measure α) :
    (∑ y ∈ f.range, μ (f ⁻¹' {y})) = μ univ

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ ∑ y ∈ f.range, μ (⇑f ⁻¹' {y}) = μ univ

Tactic:
rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_monomial_same (n : σ →₀ ℕ) (a : R) : coeff R n (monomial R n a) = a

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff R n) ((monomial R n) a) = a

Tactic:
rw [monomial_def]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff R n) ((LinearMap.single R (fun x => R) n) a) = a

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff R n) ((monomial R n) a) = a

Tactic:
classical
rw [monomial_def]
exact Pi.single_eq_same _ _

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff R n) ((LinearMap.single R (fun x => R) n) a) = a

Tactic:
exact Pi.single_eq_same _ _

Result:
no goals
-- Mathlib/NumberTheory/SiegelsLemma.lean
theorem exists_ne_zero_int_vec_norm_le'
    (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) (hA : A ≠ 0) :
    ∃ t : β → ℤ, t ≠ 0 ∧
    A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * ‖A‖) ^ ((m : ℝ) / (n - m))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ 1 ≤ ‖A‖

Tactic:
exact Int.Matrix.one_le_norm_A_of_ne_zero _ hA

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * ‖A‖) ^ e

Tactic:
have := exists_ne_zero_int_vec_norm_le A hn hm

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * ‖A‖) ^ e

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * ‖A‖) ^ e

Tactic:
rwa [max_eq_right] at this

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ 1 ≤ ‖A‖
-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem HasFPowerSeriesAt.eq_zero {p : FormalMultilinearSeries 𝕜 𝕜 E} {x : 𝕜}
    (h : HasFPowerSeriesAt 0 p x) : p = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x : 𝕜
h : HasFPowerSeriesAt 0 p x
⊢ p = 0

Tactic:
ext n x

Result:
case h.H
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ (p n) x = (0 n) x

Proof state:
case h.H
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((p n) fun x => 1)) x = (0 n) x

Tactic:
simp [h.apply_eq_zero n 1]

Result:
no goals

Proof state:
case h.H
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ (p n) x = (0 n) x

Tactic:
rw [← mkPiRing_apply_one_eq_self (p n)]

Result:
case h.H
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((p n) fun x => 1)) x = (0 n) x
-- Mathlib/Topology/Bornology/Basic.lean
@[ext]
lemma Bornology.ext (t t' : Bornology α)
    (h_cobounded : @Bornology.cobounded α t = @Bornology.cobounded α t') :
    t = t'

Proof state:
α : Type u_2
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
⊢ t = t'

Tactic:
cases t

Result:
case mk
α : Type u_2
t' : Bornology α
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ } = t'

Proof state:
case mk
α : Type u_2
t' : Bornology α
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ } = t'

Tactic:
cases t'

Result:
case mk.mk
α : Type u_2
cobounded'✝¹ : Filter α
le_cofinite'✝¹ : cobounded'✝¹ ≤ cofinite
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝¹, le_cofinite' := le_cofinite'✝¹ } =
    { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ }

Proof state:
case mk.mk
α : Type u_2
cobounded'✝¹ : Filter α
le_cofinite'✝¹ : cobounded'✝¹ ≤ cofinite
cobounded'✝ : Filter α
le_cofinite'✝ : cobounded'✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded' := cobounded'✝¹, le_cofinite' := le_cofinite'✝¹ } =
    { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem Lp.norm_const_le : ‖Lp.const p μ c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ‖(Lp.const p μ) c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
rw [← indicatorConstLp_univ]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ‖indicatorConstLp p ⋯ ⋯ c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ‖indicatorConstLp p ⋯ ⋯ c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
exact norm_indicatorConstLp_le

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Curry.lean
theorem LinearMap.curry_uncurryLeft (f : M 0 →ₗ[R] MultilinearMap R (fun i :
    Fin n => M i.succ) M₂) : f.uncurryLeft.curryLeft = f

Proof state:
case h.H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
m : M 0
x : (i : Fin n) → M i.succ
⊢ (f (Fin.cons m x 0)) x = (f m) x

Tactic:
rw [cons_zero]

Result:
no goals

Proof state:
case h.H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
m : M 0
x : (i : Fin n) → M i.succ
⊢ (f.uncurryLeft.curryLeft m) x = (f m) x

Tactic:
simp only [tail_cons, LinearMap.uncurryLeft_apply, MultilinearMap.curryLeft_apply]

Result:
case h.H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
m : M 0
x : (i : Fin n) → M i.succ
⊢ (f (Fin.cons m x 0)) x = (f m) x

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
⊢ f.uncurryLeft.curryLeft = f

Tactic:
ext m x

Result:
case h.H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
m : M 0
x : (i : Fin n) → M i.succ
⊢ (f.uncurryLeft.curryLeft m) x = (f m) x
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem mul_polyOfInterest_vars (n : ℕ) :
    ((p : 𝕄) ^ (n + 1) * polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) * polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rw [mul_polyOfInterest_aux5]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
apply remainder_vars

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
apply Subset.trans (vars_sub_subset _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
refine union_subset ?_ ?_

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ⊆ univ ×ˢ range (n + 1)

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
apply wittPolyProdRemainder_vars

Result:
no goals
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem mk_zero_right (n : ℕ) : mk K p (n, 0) = 0

Proof state:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ R K p (n, 0) (n + 1, 0)

Tactic:
have := R.intro (p := p) n (0 : K)

Result:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
this : R K p (n, 0) (n + 1, (frobenius K p) 0)
⊢ R K p (n, 0) (n + 1, 0)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
⊢ mk K p (n, 0) = 0

Tactic:
induction' n with n ih

Result:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ mk K p (0, 0) = 0

case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n + 1, 0) = 0

Proof state:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
this : R K p (n, 0) (n + 1, (frobenius K p) 0)
⊢ R K p (n, 0) (n + 1, 0)

Tactic:
rwa [frobenius_zero K p] at this

Result:
no goals

Proof state:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ mk K p (0, 0) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n, 0) = mk K p (n + 1, 0)

Tactic:
apply Quot.sound

Result:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ R K p (n, 0) (n + 1, 0)

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n + 1, 0) = 0

Tactic:
rw [← ih]

Result:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n + 1, 0) = mk K p (n, 0)

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n + 1, 0) = mk K p (n, 0)

Tactic:
symm

Result:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n, 0) = mk K p (n + 1, 0)
-- Mathlib/Data/Fin/Basic.lean
theorem cast_eq_cast (h : n = m) : (Fin.cast h : Fin n → Fin m) = _root_.cast (h ▸ rfl)

Proof state:
n : ℕ
⊢ Fin.cast ⋯ = cast ⋯

Tactic:
ext

Result:
case h.h
n : ℕ
x✝ : Fin n
⊢ ↑(Fin.cast ⋯ x✝) = ↑(cast ⋯ x✝)

Proof state:
case h.h
n : ℕ
x✝ : Fin n
⊢ ↑(Fin.cast ⋯ x✝) = ↑(cast ⋯ x✝)

Tactic:
rfl

Result:
no goals

Proof state:
n m : ℕ
h : n = m
⊢ Fin.cast h = cast ⋯

Tactic:
subst h

Result:
n : ℕ
⊢ Fin.cast ⋯ = cast ⋯
-- Mathlib/Data/List/TakeWhile.lean
theorem mem_takeWhile_imp {x : α} (hx : x ∈ takeWhile p l) : p x

Proof state:
case cons.true.inr
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true

Tactic:
exact IH hx

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
⊢ p x = true

Tactic:
cases hp : p hd

Result:
case cons.false
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = false
⊢ p x = true

case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true

Proof state:
case cons.false
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = false
⊢ p x = true

Tactic:
simp [hp] at hx

Result:
no goals

Proof state:
case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true

Tactic:
rcases hx with (rfl | hx)

Result:
case cons.true.inl
α : Type u_1
p : α → Bool
l : List α
x : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p x = true
⊢ p x = true

case cons.true.inr
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true

Proof state:
case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true

Tactic:
rw [hp, mem_cons] at hx

Result:
case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true

Proof state:
case cons.true.inl
α : Type u_1
p : α → Bool
l : List α
x : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p x = true
⊢ p x = true

Tactic:
exact hp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_of_eq_mul {u v : α → R} (φ : α → R) (hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c)
    (h : u =ᶠ[l] φ * v) :
    IsBigOWith c l u v

Proof state:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x * v x‖ ≤ c * ‖v x‖

Tactic:
refine (norm_mul_le _ _).trans ?_

Result:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖

Proof state:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v

Tactic:
simp only [IsBigOWith_def]

Result:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖

Proof state:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖

Tactic:
refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)

Result:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ (fun x a => ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)

Proof state:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ (fun x a => ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)

Tactic:
simp only [Pi.mul_apply]

Result:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x * v x‖ ≤ c * ‖v x‖
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma pow_antitone {a : A} (ha₀ : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ (fun x => a ^ x) m ≤ (fun x => a ^ x) n

Tactic:
simp only

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ a ^ m ≤ a ^ n

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
⊢ Antitone fun x => a ^ x

Tactic:
intro n m hnm

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ (fun x => a ^ x) m ≤ (fun x => a ^ x) n

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ a ^ m ≤ a ^ n

Tactic:
rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n

Tactic:
peel ha₁ with x hx _

Result:
case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : x ≤ 1
⊢ x ^ m ≤ x ^ n

Proof state:
case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
x : ℝ
hx : x ∈ spectrum ℝ a
this : x ≤ 1
⊢ x ^ m ≤ x ^ n

Tactic:
exact pow_le_pow_of_le_one (spectrum_nonneg_of_nonneg ha₀ hx) (ha₁ x hx) hnm

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n

Tactic:
rw [CFC.le_one_iff (R := ℝ) a] at ha₁

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : autoParam (0 ≤ a) _auto✝
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign

Proof state:
aig✝ : AIG Nat
assign : aig✝.CNFVar → Bool
state : State aig✝
⊢ Sat assign state ↔ CNF.Sat assign state.cnf

Tactic:
simp [State.sat_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_coe_eq_self_sub_two_pi_iff {θ : ℝ} :
    (θ : Angle).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)

Proof state:
θ : ℝ
⊢ (↑θ).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)

Tactic:
convert @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1 <;> norm_num

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep_def'' :
    iSupIndep t ↔ ∀ i, Disjoint (t i) (sSup { a | ∃ j ≠ i, t j = a })

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})

Tactic:
rw [iSupIndep_def']

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})
-- Mathlib/Data/Rat/Defs.lean
theorem divInt_eq_div (n d : ℤ) : n /. d = (n : ℚ) / d

Proof state:
n d : ℤ
⊢ n /. d = ↑n / ↑d

Tactic:
simp [div_def']

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_sub_nat (a : α) (n : ℕ) : ⌈a - n⌉ = ⌈a⌉ - n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a⌉ - ↑n

Tactic:
convert ceil_sub_int a n using 1

Result:
case h.e'_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a - ↑↑n⌉

Proof state:
case h.e'_2
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a - ↑↑n⌉

Tactic:
simp

Result:
no goals