harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma tangentCoordChange_comp {w x y z : M} {v : E}
    (h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source) :
    tangentCoordChange I x y z (tangentCoordChange I w x z v) = tangentCoordChange I w y z v

Proof state:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈
    (tangentBundleCore I M).baseSet (achart H w) ∩ (tangentBundleCore I M).baseSet (achart H x) ∩
      (tangentBundleCore I M).baseSet (achart H y)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Result:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source

Proof state:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source

Tactic:
exact h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ (tangentCoordChange I x y z) ((tangentCoordChange I w x z) v) = (tangentCoordChange I w y z) v

Tactic:
apply (tangentBundleCore I M).coordChange_comp

Result:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈
    (tangentBundleCore I M).baseSet (achart H w) ∩ (tangentBundleCore I M).baseSet (achart H x) ∩
      (tangentBundleCore I M).baseSet (achart H y)
-- Mathlib/GroupTheory/Perm/List.lean
theorem support_formPerm_le' : { x | formPerm l x ≠ x } ≤ l.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ ↑(l.toFinset ⊔ l.tail.toFinset) ≤ ↑l.toFinset

Tactic:
simpa [Finset.subset_iff] using tail_subset l

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ {x | l.formPerm x ≠ x} ≤ ↑l.toFinset

Tactic:
refine (zipWith_swap_prod_support' l l.tail).trans ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ ↑(l.toFinset ⊔ l.tail.toFinset) ≤ ↑l.toFinset
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a

Proof state:
a : Prop
inst✝ : Decidable a
this : ¬a → ¬¬a ↔ ¬¬a
⊢ ¬a → a ↔ a

Tactic:
rwa [not_not] at this

Result:
no goals

Proof state:
a : Prop
inst✝ : Decidable a
⊢ ¬a → a ↔ a

Tactic:
have := @imp_not_self (¬a)

Result:
a : Prop
inst✝ : Decidable a
this : ¬a → ¬¬a ↔ ¬¬a
⊢ ¬a → a ↔ a
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
/-- If an antitone sequence of functions has a lower bound and the sequence of integrals of these
functions tends to the integral of the lower bound, then the sequence of functions converges
almost everywhere to the lower bound. -/
lemma tendsto_of_lintegral_tendsto_of_antitone {α : Type*} {mα : MeasurableSpace α}
    {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} {μ : Measure α}
    (hf_meas : ∀ n, AEMeasurable (f n) μ)
    (hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ)))
    (hf_mono : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a))
    (h_bound : ∀ᵐ a ∂μ, ∀ i, F a ≤ f i a) (h0 : ∫⁻ a, f 0 a ∂μ ≠ ∞) :
    ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))

Tactic:
classical
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
  then h.choose else ∞
have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
  filter_upwards [h_exists] with a ha
  simp_rw [F', dif_pos ha]
  exact ha.choose_spec
suffices F' =ᵐ[μ] F by
  filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
have hF'_le : F ≤ᵐ[μ] F' := by
  filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
  exact ge_of_tendsto' h_tendsto (fun m ↦ h_le _)
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ by
  refine (ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm
  exact ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto
refine tendsto_nhds_unique ?_ hf_tendsto
exact lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), F a ∂μ ≠ ⊤

Tactic:
refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne

Result:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, F a ≤ f 0 a
-- Mathlib/Data/Rat/Lemmas.lean
theorem den_mk (n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d

Proof state:
n d : ℤ
⊢ (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d

Tactic:
have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
  rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]

Result:
n d : ℤ
this : ∀ (m : ℕ), (↑m + 1).natAbs = m + 1
⊢ (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d

Proof state:
n d : ℤ
m : ℕ
⊢ (↑m + 1).natAbs = m + 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]

Result:
no goals

Proof state:
n d : ℤ
this : ∀ (m : ℕ), (↑m + 1).natAbs = m + 1
⊢ (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d

Tactic:
rcases d with ((_ | _) | _) <;>
  simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd,
    if_neg (Nat.cast_add_one_ne_zero _), this]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem or_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs' ||| rhs' = lhs ||| rhs

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ||| rhs' = lhs ||| rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem tendsto_nhds_infty' {α : Type*} {f : OnePoint X → α} {l : Filter α} :
    Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ (↑)) (coclosedCompact X) l

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_3
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l

Tactic:
simp [nhds_infty_eq, and_comm]

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem cyclic_center_quotient_of_card_eq_prime_sq (hG : Nat.card G = p ^ 2) :
    IsCyclic (G ⧸ center G)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ Nat.card ↥(center G) * (center G).index

Tactic:
apply mul_dvd_mul_right

Result:
case h
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p ∣ Nat.card ↥(center G)

Proof state:
case h
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p ∣ Nat.card ↥(center G)

Tactic:
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩

Result:
case h.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ Nat.card ↥(center G)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ Nat.card (G ⧸ center G) ∣ p

Tactic:
rw [← mul_dvd_mul_iff_left (NeZero.ne p), ← sq, ← hG, ← (center G).card_mul_index]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ Nat.card ↥(center G) * (center G).index

Proof state:
case h.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ p ^ k

Tactic:
exact dvd_pow_self p hk0.ne'

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)

Tactic:
apply isCyclic_of_card_dvd_prime (p := p)

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ Nat.card (G ⧸ center G) ∣ p

Proof state:
case h.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ Nat.card ↥(center G)

Tactic:
rw [hk]

Result:
case h.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ p ^ k
-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma essFiniteType_iff :
    EssFiniteType R S ↔ ∃ (σ : Finset S),
      (∀ s : S, ∃ t ∈ Algebra.adjoin R (σ : Set S),
        IsUnit t ∧ s * t ∈ Algebra.adjoin R (σ : Set S))

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
constructor <;> exact fun ⟨a, b⟩ ↦ ⟨a, b⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
simp_rw [← essFiniteType_cond_iff]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem revAtFun_inj {N : ℕ} : Function.Injective (revAtFun N)

Proof state:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b

Tactic:
rw [← @revAtFun_invol N a, hab, revAtFun_invol]

Result:
no goals

Proof state:
N : ℕ
⊢ Function.Injective (revAtFun N)

Tactic:
intro a b hab

Result:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem cons_eq_cons {a b : α} {as bs : Multiset α} :
    a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Proof state:
case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs

Tactic:
intro h

Result:
case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem mem_Icc : f x ∈ Icc (0 : ℝ) 1

Proof state:
case inl
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
h : ↑f x = 0
⊢ 0 ∈ Icc 0 1

case inr
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
h : ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x ∈ Icc 0 1

Tactic:
exacts [left_mem_Icc.2 zero_le_one, ⟨f.nonneg, f.le_one⟩]

Result:
no goals

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
this : ↑f x = 0 ∨ ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ ↑f x ∈ Icc 0 1

Tactic:
rcases this with h | h <;> rw [h]

Result:
case inl
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
h : ↑f x = 0
⊢ 0 ∈ Icc 0 1

case inr
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
h : ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x ∈ Icc 0 1

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
⊢ ↑f x ∈ Icc 0 1

Tactic:
have : f x = 0 ∨ f x = _ := indicator_eq_zero_or_self _ _ _

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
this : ↑f x = 0 ∨ ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ ↑f x ∈ Icc 0 1
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma zero_comp {m : ℕ} (β : Ext Y Z m) (p : ℕ) (h : n + m = p) :
    (0 : Ext X Y n).comp β h = 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (comp 0 β h).hom = hom 0

Tactic:
simp [this, zero_hom']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ comp 0 β h = 0

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ comp 0 β h = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ comp 0 β h = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (comp 0 β h).hom = hom 0
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_insert_le {α : Type u} {s : Set α} {a : α} : #(insert a s : Set α) ≤ #s + 1

Proof state:
case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
rw [mk_insert h]

Result:
no goals

Proof state:
case pos
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
simp only [insert_eq_of_mem h, self_le_add_right]

Result:
no goals

Proof state:
α : Type u
s : Set α
a : α
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #↑(insert a s) ≤ #↑s + 1

case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p)
    (hl₁ : p = utf8Len l₁) (hl₂ : p = utf8Len l₂)
    (hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)) :
    firstDiffPos.loop ⟨l₁ ++ r₁⟩ ⟨l₂ ++ r₂⟩ ⟨stop⟩ ⟨p⟩ =
      ⟨p + utf8Len (List.takeWhile₂ (· = ·) r₁ r₂).1⟩

Proof state:
l₁ l₂ r₁ r₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)
x✝¹ x✝ : List Char
h✝ : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
h₁ : 0 < utf8Len r₁
h₂ : 0 < utf8Len r₂
h : 0 < utf8Len []
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case hnc
l₁ l₂ r₁ r₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)
x✝¹ x✝ : List Char
h : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
h₁ : 0 < utf8Len r₁
h₂ : 0 < utf8Len r₂
this : ∀ {cs : List Char}, 0 < utf8Len cs → cs ≠ []
⊢ False

Tactic:
obtain ⟨a, as, e₁⟩ := List.exists_cons_of_ne_nil (this h₁)

Result:
case hnc.intro.intro
l₁ l₂ r₁ r₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)
x✝¹ x✝ : List Char
h : ∀ (a : Char) (as : List Char) (b : Char) (bs : List Char), r₁ = a :: as → r₂ = b :: bs → False
h₁ : 0 < utf8Len r₁
h₂ : 0 < utf8Len r₂
this : ∀ {cs : List Char}, 0 < utf8Len cs → cs ≠ []
a : Char
as : List Char
e₁ : r₁ = a :: as
⊢ False

Proof state:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (a :: r₂))
⊢ p + a.utf8Size = utf8Len (l₁ ++ [a])

Tactic:
simp [hl₁]

Result:
no goals

Proof state:
l₁ l₂ : List Char
stop p : Nat
hl₁ : p = utf8Len l₁
hl₂ : p = utf8Len l₂
x✝¹ x✝ : List Char
a : Char
r₁ : List Char
b : Char
r₂ : List Char
hstop : stop = min (utf8Len l₁ + utf8Len (a :: r₁)) (utf8Len l₂ + utf8Len (b :: r₂))
⊢ { data := l₁ ++ a :: r₁ }.get { byteIdx := p } = a

Tactic:
simp [hl₁, get_of_valid]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_add_one (n : ℤ) : C R (n + 1) = X * C R n - C R (n - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ C R (n + 1) = X * C R n - C R (n - 1)

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 1)

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_of_splits [DecidableEq E] (h : f.Splits (algebraMap F E)) :
    f.natSepDegree = (f.aroots E).toFinset.card

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
inst✝ : DecidableEq E
h : Splits (algebraMap F E) f
⊢ f.natSepDegree = (f.aroots E).toFinset.card

Tactic:
rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
  roots_map _ ((splits_id_iff_splits _).mpr <| SplittingField.splits f),
  Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
inst✝ : DecidableEq E
h : Splits (algebraMap F E) f
⊢ f.natSepDegree = (f.aroots E).toFinset.card

Tactic:
classical
rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
  roots_map _ ((splits_id_iff_splits _).mpr <| SplittingField.splits f),
  Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem Fin.prod_univ_eq_prod_range [CommMonoid α] (f : ℕ → α) (n : ℕ) :
    ∏ i : Fin n, f i = ∏ i ∈ range n, f i :=
  calc
    ∏ i : Fin n, f i = ∏ i : { x // x ∈ range n }, f i :=
      Fintype.prod_equiv (Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))) _ _ (by simp)
    _ = ∏ i ∈ range n, f i

Proof state:
α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : Fin n), f ↑x = f ↑((equivSubtype.trans (Equiv.subtypeEquivRight ⋯)) x)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i : { x // x ∈ range n }, f ↑i = ∏ i ∈ range n, f i

Tactic:
rw [← attach_eq_univ, prod_attach]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.uniformEquicontinuousOn_iff_right {p : κ → Prop}
    {s : κ → Set (α × α)} {F : ι → β → α} {S : Set β} (hα : (𝓤 α).HasBasis p s) :
    UniformEquicontinuousOn F S ↔
      ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ s k

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
  (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
          ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
S : Set β
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
          ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp]
lemma toFinset_Ioi (a : α) [Fintype (Ioi a)] : (Ioi a).toFinset = Finset.Ioi a

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
⊢ (Ioi a).toFinset = Finset.Ioi a

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
a✝ : α
⊢ a✝ ∈ (Ioi a).toFinset ↔ a✝ ∈ Finset.Ioi a

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
a✝ : α
⊢ a✝ ∈ (Ioi a).toFinset ↔ a✝ ∈ Finset.Ioi a

Tactic:
simp

Result:
no goals