harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
theorem binomial_apply_zero (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) :
    binomial p h n 0 = (1-p)^n

Proof state:
p : ℝ≥0∞
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) 0 = (1 - p) ^ n

Tactic:
simp [binomial_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b

Proof state:
b : Bool
⊢ (ofBool b)[0] = b

Tactic:
rw [getElem_eq_iff, getElem?_zero_ofBool]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem card_dvd_card_image₂_left (hf : ∀ b ∈ t, Injective fun a => f a b)
    (ht : ((fun b => s.image fun a => f a b) '' t).PairwiseDisjoint id) :
    #s ∣ #(image₂ f s t)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a => f a b
ht : ((fun b => image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ (fun b a => f a b) t s)

Tactic:
exact card_dvd_card_image₂_right hf ht

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a => f a b
ht : ((fun b => image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ f s t)

Tactic:
rw [← image₂_swap]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a => f a b
ht : ((fun b => image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ (fun b a => f a b) t s)
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma zero_not_mem_coeffs (p : MvPolynomial σ R) : 0 ∉ p.coeffs

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
⊢ False

Tactic:
obtain ⟨n, hnsupp, hn⟩ := mem_coeffs_iff.mp hz

Result:
case intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
n : σ →₀ ℕ
hnsupp : n ∈ p.support
hn : 0 = coeff n p
⊢ False

Proof state:
case intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
n : σ →₀ ℕ
hnsupp : n ∈ p.support
hn : 0 = coeff n p
⊢ False

Tactic:
exact (mem_support_iff.mp hnsupp) hn.symm

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ 0 ∉ p.coeffs

Tactic:
intro hz

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
⊢ False
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem condExp_prod_ae_eq_integral_condDistrib₀ [NormedSpace ℝ F] [CompleteSpace F]
    (hX : Measurable X) (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a)))
    (hf_int : Integrable (fun a => f (X a, Y a)) μ) :
    μ[fun a => f (X a, Y a)|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) :=
  haveI hf_int' : Integrable f (μ.map fun a => (X a, Y a))

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int : Integrable (fun a => f (X a, Y a)) μ
⊢ Integrable f (Measure.map (fun a => (X a, Y a)) μ)

Tactic:
rwa [integrable_map_measure hf (hX.aemeasurable.prod_mk hY)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem sum_pointWeightsWithCircumcenter {n : ℕ} (i : Fin (n + 1)) :
    ∑ j, pointWeightsWithCircumcenter i j = 1

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ ∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j = 1

Tactic:
convert sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j

Result:
case h.e'_2.a
n : ℕ
i : Fin (n + 1)
j : PointsWithCircumcenterIndex n
a✝ : j ∈ univ
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

case h.e'_3
n : ℕ
i : Fin (n + 1)
⊢ 1 = if pointIndex i ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i) else 0

Proof state:
case h.e'_3
n : ℕ
i : Fin (n + 1)
⊢ 1 = if pointIndex i ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i) else 0

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.a
n : ℕ
i : Fin (n + 1)
j : PointsWithCircumcenterIndex n
a✝ : j ∈ univ
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

Tactic:
cases j <;> simp [pointWeightsWithCircumcenter]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem forall_neBot_le_iff {g : Filter α} {p : Filter α → Prop} (hp : Monotone p) :
    (∀ f : Filter α, NeBot f → f ≤ g → p f) ↔ ∀ f : Ultrafilter α, ↑f ≤ g → p f

Proof state:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), f.NeBot → f ≤ g → p f

Tactic:
intro H f hf hfg

Result:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : f.NeBot
hfg : f ≤ g
⊢ p f

Proof state:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f

Tactic:
refine ⟨fun H f hf => H f f.neBot hf, ?_⟩

Result:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), f.NeBot → f ≤ g → p f

Proof state:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : f.NeBot
hfg : f ≤ g
⊢ p f

Tactic:
exact hp (of_le f) (H _ ((of_le f).trans hfg))

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
lemma dlo_isExtensionPair
    (M : Type w) [Language.order.Structure M] [M ⊨ Language.order.linearOrderTheory]
    (N : Type w') [Language.order.Structure N] [N ⊨ Language.order.dlo] [Nonempty N] :
    Language.order.IsExtensionPair M N

Proof state:
case h.e'_2.h.e'_4
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
g : { x // x ∈ insert m hS.toFinset } ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
⊢ (Substructure.closure Language.order).toFun {m} ⊔ S =
    (Substructure.closure Language.order).toFun ↑(insert m hS.toFinset)

Tactic:
simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
  Substructure.closure_eq]

Result:
no goals

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝³ : LinearOrder M := Language.order.linearOrderOfModels M
this✝² : LinearOrder N := Language.order.linearOrderOfModels N
this✝¹ : DenselyOrdered N
this✝ : NoBotOrder N
this : NoTopOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have := NoBotOrder.to_noMinOrder N

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁴ : LinearOrder M := Language.order.linearOrderOfModels M
this✝³ : LinearOrder N := Language.order.linearOrderOfModels N
this✝² : DenselyOrdered N
this✝¹ : NoBotOrder N
this✝ : NoTopOrder N
this : NoMinOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
letI := Language.order.linearOrderOfModels M

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this : LinearOrder M := Language.order.linearOrderOfModels M
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem induction_on [AddMonoid G] {p : k[G] → Prop} (f : k[G])
    (hM : ∀ g, p (of k G (Multiplicative.ofAdd g)))
    (hadd : ∀ f g : k[G], p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f

Proof state:
case refine_2
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
g : G
r : k
⊢ p (Finsupp.single g r)

Tactic:
convert hsmul r (of k G (Multiplicative.ofAdd g)) (hM g)

Result:
case h.e'_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
g : G
r : k
⊢ Finsupp.single g r = r • (of k G) (Multiplicative.ofAdd g)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
⊢ p f

Tactic:
refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_

Result:
case refine_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
⊢ p 0

case refine_2
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
g : G
r : k
⊢ p (Finsupp.single g r)

Proof state:
case h.e'_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
g : G
r : k
⊢ Finsupp.single g r = r • (of k G) (Multiplicative.ofAdd g)

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddMonoid G
p : k[G] → Prop
f : k[G]
hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))
hadd : ∀ (f g : k[G]), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)
⊢ p 0

Tactic:
simpa using hsmul 0 (of k G (Multiplicative.ofAdd 0)) (hM 0)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem norm_integral_le_integral_norm (f : α → G) : ‖∫ a, f a ∂μ‖ ≤ ∫ a, ‖f a‖ ∂μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
by_cases h : AEStronglyMeasurable f μ

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
have le_ae : ∀ᵐ a ∂μ, 0 ≤ ‖f a‖ := Eventually.of_forall fun a => norm_nonneg _

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ 0 ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
exact integral_nonneg_of_ae le_ae

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
rw [integral_non_aestronglyMeasurable h, norm_zero]

Result:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ 0 ≤ ∫ (a : α), ‖f a‖ ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
calc
  ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) :=
    norm_integral_le_lintegral_norm _
  _ = ∫ a, ‖f a‖ ∂μ := (integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inr_f_fst_v (p q : ℤ) (hpq : p + 1 = q) :
    (inr φ).f p ≫ (fst φ).1.v p q hpq = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (inr φ).f p ≫ (↑(fst φ)).v p q hpq = 0

Tactic:
simp [inr, fst]

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem J_inv : (J l R)⁻¹ = -J l R

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * -J l R = 1

Tactic:
rw [Matrix.mul_neg, J_squared]

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ - -1 = 1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ - -1 = 1

Tactic:
exact neg_neg 1

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (J l R)⁻¹ = -J l R

Tactic:
refine Matrix.inv_eq_right_inv ?_

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * -J l R = 1
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
/-- The multiplicative indicators of δ-thickenings of a set tend pointwise to the multiplicative
indicator of the set, as δ>0 tends to zero. -/
@[to_additive "The indicators of δ-thickenings of a set tend pointwise to the indicator of the
set, as δ>0 tends to zero."]
lemma tendsto_mulIndicator_thickening_mulIndicator_closure (f : α → β) (E : Set α) :
    Tendsto (fun δ ↦ (Metric.thickening δ E).mulIndicator f) (𝓝[>] 0)
      (𝓝 ((closure E).mulIndicator f))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => (thickening i E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))

Tactic:
rw [tendsto_congr' (mulIndicator_thickening_eventually_eq_mulIndicator_closure f E x)]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => (closure E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ => (thickening δ E).mulIndicator f) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f))

Tactic:
rw [tendsto_pi_nhds]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => (thickening i E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => (thickening i E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))

Tactic:
intro x

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => (thickening i E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => (closure E).mulIndicator f x) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f x))

Tactic:
apply tendsto_const_nhds

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldr_ext (f g : α → β → β) (b : β) {l : List α} (H : ∀ a ∈ l, ∀ b : β, f a b = g a b) :
    foldr f b l = foldr g b l

Proof state:
α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l

Tactic:
induction' l with hd tl ih

Result:
case nil
α : Type u
β : Type v
f g : α → β → β
b : β
H : ∀ (a : α), a ∈ [] → ∀ (b : β), f a b = g a b
⊢ foldr f b [] = foldr g b []

case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Proof state:
case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Tactic:
simp only [foldr, ih H.2, H.1]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
f g : α → β → β
b : β
H : ∀ (a : α), a ∈ [] → ∀ (b : β), f a b = g a b
⊢ foldr f b [] = foldr g b []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Tactic:
simp only [mem_cons, or_imp, forall_and, forall_eq] at H

Result:
case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr : |r| < 1) :
    Tendsto (fun n ↦ (n : ℝ) ^ k * r ^ n : ℕ → ℝ) atTop (𝓝 0)

Proof state:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun x => ‖↑x ^ k * r ^ x‖) atTop (𝓝 0)

Proof state:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun x => ‖↑x ^ k * r ^ x‖) atTop (𝓝 0)

Tactic:
simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'

Result:
no goals

Proof state:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => 0 = (fun n => ↑n ^ k * r ^ n) x) x}

Tactic:
simp [zero_lt_one.trans_le hn |>.ne', h0]

Result:
no goals

Proof state:
k : ℕ
r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
by_cases h0 : r = 0

Result:
case pos
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

Proof state:
case pos
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds.congr'
  (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn |>.ne', h0]⟩)

Result:
no goals

Proof state:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
have hr' : 1 < |r|⁻¹ := (one_lt_inv₀ (abs_pos.2 h0)).2 hr

Result:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_adjoin_simple_dvd_finrank (α : E) :
    finSepDegree F F⟮α⟯ ∣ finrank F F⟮α⟯

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank F ↥F⟮α⟯ = 0
⊢ finSepDegree F ↥F⟮α⟯ ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank F ↥F⟮α⟯ = 0
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯

Tactic:
rw [this]

Result:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank F ↥F⟮α⟯ = 0
⊢ finSepDegree F ↥F⟮α⟯ ∣ 0

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯

Tactic:
rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral]

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).natSepDegree ∣ (minpoly F α).natDegree

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯

Tactic:
have : finrank F F⟮α⟯ = 0 := finrank_of_infinite_dimensional fun _ ↦
  halg ((AdjoinSimple.isIntegral_gen F α).1 (IsIntegral.of_finite F _)).isAlgebraic

Result:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank F ↥F⟮α⟯ = 0
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).natSepDegree ∣ (minpoly F α).natDegree

Tactic:
exact (minpoly.irreducible halg.isIntegral).natSepDegree_dvd_natDegree

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯

Tactic:
by_cases halg : IsAlgebraic F α

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯

case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯
-- Mathlib/Data/Finset/Prod.lean
theorem subset_product_image_snd [DecidableEq β] : (s ×ˢ t).image Prod.snd ⊆ t := fun i => by
  simp +contextual [mem_image]

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t

Tactic:
simp +contextual [mem_image]

Result:
no goals