harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.aemeasurable {β : Type*} [MeasurableSpace β] [l.IsCountablyGenerated] [l.NeBot]
    {f : α → β} {φ : ι → Set α} (hφ : AECover μ l φ)
    (hfm : ∀ i, AEMeasurable f (μ.restrict <| φ i)) : AEMeasurable f μ

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
⊢ AEMeasurable f μ

Tactic:
obtain ⟨u, hu⟩ := l.exists_seq_tendsto

Result:
case intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEMeasurable f μ

Proof state:
case intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ i, φ (u i)))
⊢ AEMeasurable f μ

Tactic:
rwa [Measure.restrict_eq_self_of_ae_mem] at this

Result:
case intro.hs
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ i, φ (u i)))
⊢ ∀ᵐ (x : α) ∂μ, x ∈ ⋃ i, φ (u i)

Proof state:
case intro.hs
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ i, φ (u i)))
⊢ ∀ᵐ (x : α) ∂μ, x ∈ ⋃ i, φ (u i)

Tactic:
filter_upwards [hφ.ae_eventually_mem] with x hx using
  mem_iUnion.mpr (hu.eventually hx).exists

Result:
no goals

Proof state:
case intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEMeasurable f μ

Tactic:
have := aemeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)

Result:
case intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ i, φ (u i)))
⊢ AEMeasurable f μ
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean
theorem tendsto_measure_thickening {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (thickening R s) ≠ ∞) :
    Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), thickening δ s)))

Tactic:
exact tendsto_measure_biInter_gt (fun r _ => isOpen_thickening.nullMeasurableSet)
    (fun i j _ ij => thickening_mono ij _) hs

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))

Tactic:
rw [closure_eq_iInter_thickening]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ⊤
⊢ Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), thickening δ s)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_set {l : List α} {i : Nat} {a : α} :
    (l.set i a).mapIdx f = (l.mapIdx f).set i (f i a)

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i : Nat
a : α
⊢ ∀ (i_1 : Nat),
    (if i = i_1 then if i < l.length then some (f i a) else none else Option.map (f i_1) l[i_1]?) =
      Option.map (f i_1) (if i = i_1 then if i < l.length then some a else none else l[i_1]?)

Tactic:
intro i

Result:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i✝ : Nat
a : α
i : Nat
⊢ (if i✝ = i then if i✝ < l.length then some (f i✝ a) else none else Option.map (f i) l[i]?) =
    Option.map (f i) (if i✝ = i then if i✝ < l.length then some a else none else l[i]?)

Proof state:
case isFalse
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i✝ : Nat
a : α
i : Nat
h✝ : ¬i✝ = i
⊢ Option.map (f i) l[i]? = Option.map (f i) l[i]?

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i : Nat
a : α
⊢ mapIdx f (l.set i a) = (mapIdx f l).set i (f i a)

Tactic:
simp only [mapIdx_eq_iff, getElem?_set, length_mapIdx, getElem?_mapIdx]

Result:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i : Nat
a : α
⊢ ∀ (i_1 : Nat),
    (if i = i_1 then if i < l.length then some (f i a) else none else Option.map (f i_1) l[i_1]?) =
      Option.map (f i_1) (if i = i_1 then if i < l.length then some a else none else l[i_1]?)

Proof state:
case isTrue
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i✝ : Nat
a : α
i : Nat
h✝ : i✝ = i
⊢ (if i✝ < l.length then some (f i✝ a) else none) = Option.map (f i) (if i✝ < l.length then some a else none)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i✝ : Nat
a : α
i : Nat
⊢ (if i✝ = i then if i✝ < l.length then some (f i✝ a) else none else Option.map (f i) l[i]?) =
    Option.map (f i) (if i✝ = i then if i✝ < l.length then some a else none else l[i]?)

Tactic:
split

Result:
case isTrue
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i✝ : Nat
a : α
i : Nat
h✝ : i✝ = i
⊢ (if i✝ < l.length then some (f i✝ a) else none) = Option.map (f i) (if i✝ < l.length then some a else none)

case isFalse
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i✝ : Nat
a : α
i : Nat
h✝ : ¬i✝ = i
⊢ Option.map (f i) l[i]? = Option.map (f i) l[i]?
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem iso_w {f g : Arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : e.inv.right ≫ e.hom.right = 𝟙 g.right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right

Tactic:
rw [Arrow.w_assoc, eq, Category.comp_id]

Result:
no goals

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : (e.inv ≫ e.hom).right = (𝟙 g).right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right

Tactic:
rw [Arrow.comp_right, Arrow.id_right] at eq

Result:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : e.inv.right ≫ e.hom.right = 𝟙 g.right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right

Tactic:
have eq := Arrow.hom.congr_right e.inv_hom_id

Result:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : (e.inv ≫ e.hom).right = (𝟙 g).right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
-- Mathlib/Combinatorics/Enumerative/Partition.lean
@[simp] lemma ofSym_map (e : σ ≃ τ) (s : Sym σ n) :
    ofSym (s.map e) = ofSym s

Proof state:
case e_f.h
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
i : σ
⊢ count (e i) (map ⇑e ↑s) = count i ↑s

Tactic:
rw [← Multiset.count_map_eq_count' e _ e.injective]

Result:
no goals

Proof state:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x => count x (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun x => count x ↑s) (↑s).dedup

Tactic:
simp only [map_map, Function.comp_apply]

Result:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x => count (e x) (map ⇑e ↑s)) (↑s).dedup = map (fun x => count x ↑s) (↑s).dedup

Proof state:
case e_f
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ (fun x => count (e x) (map ⇑e ↑s)) = fun x => count x ↑s

Tactic:
funext i

Result:
case e_f.h
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
i : σ
⊢ count (e i) (map ⇑e ↑s) = count i ↑s

Proof state:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x => count (e x) (map ⇑e ↑s)) (↑s).dedup = map (fun x => count x ↑s) (↑s).dedup

Tactic:
congr

Result:
case e_f
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ (fun x => count (e x) (map ⇑e ↑s)) = fun x => count x ↑s

Proof state:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ ofSym (Sym.map (⇑e) s) = ofSym s

Tactic:
simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, toFinset_val, mk.injEq]

Result:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x => count x (map ⇑e ↑s)) (map ⇑e ↑s).dedup = map (fun x => count x ↑s) (↑s).dedup

Proof state:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x => count x (map ⇑e ↑s)) (map ⇑e ↑s).dedup = map (fun x => count x ↑s) (↑s).dedup

Tactic:
rw [Multiset.dedup_map_of_injective e.injective]

Result:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x => count x (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun x => count x ↑s) (↑s).dedup
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem comp_p {P Q : Karoubi C} (f : Hom P Q) : f.f ≫ Q.p = f.f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ f.f ≫ Q.p = f.f

Tactic:
rw [f.comm, assoc, assoc, Q.idem]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_toReal (θ : Angle) : Real.sin θ.toReal = sin θ

Proof state:
θ : Angle
⊢ Real.sin θ.toReal = θ.sin

Tactic:
conv_rhs => rw [← coe_toReal θ, sin_coe]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x

Tactic:
simp only [fderivWithin, differentiableWithinAt_congr_set' _ h, hasFDerivWithinAt_congr_set' _ h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x

Tactic:
classical
simp only [fderivWithin, differentiableWithinAt_congr_set' _ h, hasFDerivWithinAt_congr_set' _ h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem isQuotientQuotient (S : AddSubgroup M) : IsQuotient S.normedMk :=
  ⟨S.surjective_normedMk, fun m => by simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m⟩

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ = sInf ((fun m_1 => ‖m + m_1‖) '' ↑S.normedMk.ker)

Tactic:
simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_flatMap {f : α → Array β} {b} {l : Array α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
b : β
l : Array α
⊢ b ∈ flatMap f l ↔ ∃ a, a ∈ l ∧ b ∈ f a

Tactic:
simp [flatMap_def, mem_flatten]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
b : β
l : Array α
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
b : β
l : Array α
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a

Tactic:
exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem posMulReflectLE_iff_mulPosReflectLE : PosMulReflectLE α ↔ MulPosReflectLE α

Proof state:
α : Type u_3
inst✝³ : Mul α
inst✝² : Std.Commutative fun x1 x2 => x1 * x2
inst✝¹ : Zero α
inst✝ : Preorder α
⊢ PosMulReflectLE α ↔ MulPosReflectLE α

Tactic:
simp only [posMulReflectLE_iff, mulPosReflectLE_iff, Std.Commutative.comm]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mk_dvd_mk {a b : M} : Associates.mk a ∣ Associates.mk b ↔ a ∣ b

Proof state:
case mpr.intro
M : Type u_1
inst✝ : CommMonoid M
a c : M
⊢ ∃ x, a * x ~ᵤ a * c

Tactic:
use c

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) → ∃ c, b = a * c

Tactic:
rintro ⟨x, u, rfl⟩

Result:
case mp.intro.intro
M : Type u_1
inst✝ : CommMonoid M
a x : M
u : Mˣ
⊢ ∃ c, a * x * ↑u = a * c

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b

Tactic:
rintro ⟨c, rfl⟩

Result:
case mpr.intro
M : Type u_1
inst✝ : CommMonoid M
a c : M
⊢ ∃ x, a * x ~ᵤ a * c

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ Associates.mk a ∣ Associates.mk b ↔ a ∣ b

Tactic:
simp only [dvd_def, mk_surjective.exists, mk_mul_mk, mk_eq_mk_iff_associated,
  Associated.comm (x := b)]

Result:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) ↔ ∃ c, b = a * c

Proof state:
case mp.intro.intro
M : Type u_1
inst✝ : CommMonoid M
a x : M
u : Mˣ
⊢ ∃ c, a * x * ↑u = a * c

Tactic:
exact ⟨_, mul_assoc ..⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) ↔ ∃ c, b = a * c

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) → ∃ c, b = a * c

case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_pos_of_dvd (hdiv : a ∣ b) : 0 < multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
nh : ¬FiniteMultiplicity a b
⊢ False

Tactic:
simp [nh] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ FiniteMultiplicity a b

Tactic:
by_contra! nh

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
nh : ¬FiniteMultiplicity a b
⊢ False

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False

Tactic:
simpa [hdiv] using FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
  (by by_contra! nh; simp [nh] at h) (lt_one_iff.mpr h)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
⊢ 0 < multiplicity a b

Tactic:
refine Nat.pos_iff_ne_zero.2 fun h => ?_

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False
-- Mathlib/Order/InitialSeg.lean
theorem acc (f : r ≼i s) (a : α) : Acc r a ↔ Acc s (f a) :=
  ⟨by
    refine fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_
    obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb
    exact ha _ (f.map_rel_iff.mp hb), f.toRelEmbedding.acc a⟩

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
b : β
hb : s b (f a)
⊢ Acc s b

Tactic:
obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
a' : α
hb : s (f a') (f a)
⊢ Acc s (f a')

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
⊢ Acc r a → Acc s (f a)

Tactic:
refine fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
b : β
hb : s b (f a)
⊢ Acc s b

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
a' : α
hb : s (f a') (f a)
⊢ Acc s (f a')

Tactic:
exact ha _ (f.map_rel_iff.mp hb)

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_isStrictRestriction {M : Matroid α} (hR : R ⊂ M.E) : M ↾ R <r M

Proof state:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ R
h : M ↾ R = M
⊢ False

Tactic:
exact hR.ne rfl

Result:
no goals

Proof state:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
⊢ M ↾ R <r M

Tactic:
refine (M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)

Result:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
h : M ↾ R = M
⊢ False

Proof state:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
h : M ↾ R = M
⊢ False

Tactic:
rw [← h, restrict_ground_eq] at hR

Result:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ R
h : M ↾ R = M
⊢ False
-- Mathlib/Order/Atoms.lean
theorem covBy_iff {K L : A} :
    K ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
rw [lt_iff_le_not_le, lt_iff_le_and_ne, and_and_and_comm]

Result:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
push_neg

Result:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_

Result:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
  SetLike.not_le_iff_exists, and_comm, implies_true]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- `𝓞 K ⧸ Ideal.span {ζ - 1}` is finite. -/
lemma finite_quotient_toInteger_sub_one [NumberField K] {k : ℕ+} (hk : 1 < k)
    (hζ : IsPrimitiveRoot ζ k) : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
h : hζ.toInteger = 1
⊢ False

Tactic:
exact hζ.ne_one hk (RingOfIntegers.ext_iff.1 h)

Result:
no goals

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
h : Ideal.span {hζ.toInteger - 1} = ⊥
⊢ False

Tactic:
simp only [Ideal.span_singleton_eq_bot, sub_eq_zero, ← Subtype.coe_inj] at h

Result:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
h : hζ.toInteger = 1
⊢ False

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
⊢ Fintype (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Tactic:
refine Ideal.fintypeQuotientOfFreeOfNeBot _ (fun h ↦ ?_)

Result:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
h : Ideal.span {hζ.toInteger - 1} = ⊥
⊢ False

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Tactic:
refine (finite_iff_nonempty_fintype _).2 ⟨?_⟩

Result:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
⊢ Fintype (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem Filter.Tendsto.const_cpow {l : Filter α} {f : α → ℂ} {a b : ℂ} (hf : Tendsto f l (𝓝 b))
    (h : a ≠ 0 ∨ b ≠ 0) : Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))

Proof state:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))

Tactic:
cases h with
| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf

Result:
no goals

Proof state:
case inl
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))

Tactic:
exact (continuousAt_const_cpow h).tendsto.comp hf

Result:
no goals

Proof state:
case inr
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))

Tactic:
exact (continuousAt_const_cpow' h).tendsto.comp hf

Result:
no goals
-- Mathlib/RingTheory/RingHom/Surjective.lean
theorem surjective_respectsIso : RespectsIso surjective

Proof state:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective ⇑e.toRingHom

Tactic:
intros _ _ _ _ e

Result:
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e : R✝ ≃+* S✝
⊢ Function.Surjective ⇑e.toRingHom

Proof state:
⊢ RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f

Tactic:
apply surjective_stableUnderComposition.respectsIso

Result:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective ⇑e.toRingHom

Proof state:
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e : R✝ ≃+* S✝
⊢ Function.Surjective ⇑e.toRingHom

Tactic:
exact e.surjective

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem mem_interleave_right {a : α} {s₁ : Stream' α} (s₂ : Stream' α) : a ∈ s₂ → a ∈ s₁ ⋈ s₂ :=
  fun ⟨n, h⟩ => Exists.intro (2 * n + 1) (by rw [h, get_interleave_right])

Proof state:
α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₂
n : ℕ
h : (fun b => a = b) (s₂.get n)
⊢ (fun b => a = b) ((s₁ ⋈ s₂).get (2 * n + 1))

Tactic:
rw [h, get_interleave_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_map_le (f : M →ₗ[R] M₁) (p : Submodule R M) :
    Module.rank R (p.map f) ≤ Module.rank R p

Proof state:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

Tactic:
simpa using lift_rank_map_le f p

Result:
no goals