harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Complement.lean
theorem isComplement_univ_right : IsComplement S univ ↔ ∃ g : G, S = {g}

Proof state:
case refine_1.intro
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : ↑S × ↑univ
h✝ : (fun x => ↑x.1 * ↑x.2) a = 1
⊢ S.Nonempty

Tactic:
exact ⟨a.1.1, a.1.2⟩

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
⊢ S.Nonempty

Tactic:
obtain ⟨a, _⟩ := h.2 1

Result:
case refine_1.intro
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : ↑S × ↑univ
h✝ : (fun x => ↑x.1 * ↑x.2) a = 1
⊢ S.Nonempty

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
⊢ IsComplement S univ ↔ ∃ g, S = {g}

Tactic:
refine
  ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩

Result:
case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
⊢ S.Nonempty

case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement S univ

Proof state:
case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement S univ

Tactic:
rintro ⟨g, rfl⟩

Result:
case refine_3.intro
G : Type u_1
inst✝ : Group G
g : G
⊢ IsComplement {g} univ

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this : (⟨a, ha⟩, ⟨a⁻¹, ⋯⟩) = (⟨b, hb⟩, ⟨b⁻¹, ⋯⟩)
⊢ a = b

Tactic:
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).1

Result:
no goals

Proof state:
case refine_3.intro
G : Type u_1
inst✝ : Group G
g : G
⊢ IsComplement {g} univ

Tactic:
exact isComplement_singleton_univ

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

Tactic:
have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : Set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
  h.1 ((mul_inv_cancel a).trans (mul_inv_cancel b).symm)

Result:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this : (⟨a, ha⟩, ⟨a⁻¹, ⋯⟩) = (⟨b, hb⟩, ⟨b⁻¹, ⋯⟩)
⊢ a = b
-- Mathlib/Data/Nat/Init.lean
@[simp, nolint simpNF] protected lemma add_eq_right : a + b = b ↔ a = 0

Proof state:
a b : ℕ
⊢ a + b = b ↔ a = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem bitwise_swap {f : Bool → Bool → Bool} :
    bitwise (Function.swap f) = Function.swap (bitwise f)

Proof state:
case h.h.ind.succ.succ
f : Bool → Bool → Bool
m n : ℕ
ih : ∀ (n : ℕ), bitwise (swap f) ((m + 1) / 2) n = bitwise f n ((m + 1) / 2)
⊢ bitwise (swap f) (m + 1) (n + 1) = bitwise f (n + 1) (m + 1)

Tactic:
simp [bitwise_of_ne_zero, ih]

Result:
no goals

Proof state:
case h.h.ind
f : Bool → Bool → Bool
m : ℕ
ih : ∀ (m_1 : ℕ), m_1 < m → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1
n : ℕ
⊢ bitwise (swap f) m n = bitwise f n m

Tactic:
rcases m with - | m
<;> rcases n with - | n
<;> try rw [bitwise_zero_left, bitwise_zero_right]

Result:
case h.h.ind.succ.succ
f : Bool → Bool → Bool
m : ℕ
ih : ∀ (m_1 : ℕ), m_1 < m + 1 → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1
n : ℕ
⊢ bitwise (swap f) (m + 1) (n + 1) = bitwise f (n + 1) (m + 1)

Proof state:
f : Bool → Bool → Bool
⊢ bitwise (swap f) = swap (bitwise f)

Tactic:
funext m n

Result:
case h.h
f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap f) m n = swap (bitwise f) m n

Proof state:
case h.h.ind.succ.zero
f : Bool → Bool → Bool
m : ℕ
ih : ∀ (m_1 : ℕ), m_1 < m + 1 → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1
⊢ bitwise (swap f) (m + 1) 0 = bitwise f 0 (m + 1)

Tactic:
rw [bitwise_zero_left, bitwise_zero_right]

Result:
no goals

Proof state:
case h.h
f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap f) m n = swap (bitwise f) m n

Tactic:
simp only [Function.swap]

Result:
case h.h
f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap f) m n = bitwise f n m

Proof state:
case h.h.ind.succ.succ
f : Bool → Bool → Bool
m : ℕ
ih : ∀ (m_1 : ℕ), m_1 < m + 1 → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1
n : ℕ
⊢ bitwise (swap f) (m + 1) (n + 1) = bitwise f (n + 1) (m + 1)

Tactic:
specialize ih ((m+1) / 2) (div_lt_self' ..)

Result:
case h.h.ind.succ.succ
f : Bool → Bool → Bool
m n : ℕ
ih : ∀ (n : ℕ), bitwise (swap f) ((m + 1) / 2) n = bitwise f n ((m + 1) / 2)
⊢ bitwise (swap f) (m + 1) (n + 1) = bitwise f (n + 1) (m + 1)

Proof state:
case h.h
f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap f) m n = bitwise f n m

Tactic:
induction' m using Nat.strongRecOn with m ih generalizing n

Result:
case h.h.ind
f : Bool → Bool → Bool
m : ℕ
ih : ∀ (m_1 : ℕ), m_1 < m → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1
n : ℕ
⊢ bitwise (swap f) m n = bitwise f n m
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma add_one_ediv_two_mul_two_of_odd : Odd n → 1 + n / 2 * 2 = n

Proof state:
case h.e'_2.h.e'_6
c : ℤ
⊢ 1 = (2 * c + 1) % 2

Tactic:
simp [Int.add_emod]

Result:
no goals

Proof state:
case intro
c : ℤ
⊢ 1 + (2 * c + 1) / 2 * 2 = 2 * c + 1

Tactic:
rw [add_comm]

Result:
case intro
c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1

Proof state:
n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n

Tactic:
rintro ⟨c, rfl⟩

Result:
case intro
c : ℤ
⊢ 1 + (2 * c + 1) / 2 * 2 = 2 * c + 1

Proof state:
case intro
c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1

Tactic:
convert Int.ediv_add_emod' (2 * c + 1) 2

Result:
case h.e'_2.h.e'_6
c : ℤ
⊢ 1 = (2 * c + 1) % 2
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_deriv_of_nonpos (hcont : ContinuousWithinAt g (Ici a) a)
    (hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x) (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0)
    (hg : Tendsto g atTop (𝓝 l)) : IntegrableOn g' (Ioi a)

Proof state:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a) volume

Tactic:
apply integrable_neg_iff.1

Result:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ Integrable (-g') (volume.restrict (Ioi a))

Proof state:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ Integrable (-g') (volume.restrict (Ioi a))

Tactic:
exact integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
  (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
@[simp] lemma ae_eq_top  : ae μ = ⊤ ↔ ∀ a, μ {a} ≠ 0

Proof state:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
⊢ μ univᶜ = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ s = univ

Tactic:
rw [← compl_empty_iff, ← not_nonempty_iff_eq_empty]

Result:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ ¬sᶜ.Nonempty

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (s : Set α), μ sᶜ = 0 ↔ s = univ
a : α
ha : μ {a} = 0
⊢ False

Tactic:
simpa [ha] using (h {a}ᶜ).1

Result:
no goals

Proof state:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ ¬sᶜ.Nonempty

Tactic:
rintro ⟨a, ha⟩

Result:
case refine_1.intro
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
a : α
ha : a ∈ sᶜ
⊢ False

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
⊢ ae μ = ⊤ ↔ ∀ (a : α), μ {a} ≠ 0

Tactic:
simp only [Filter.ext_iff, mem_ae_iff, mem_top, ne_eq]

Result:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
⊢ (∀ (s : Set α), μ sᶜ = 0 ↔ s = univ) ↔ ∀ (a : α), ¬μ {a} = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
⊢ (∀ (s : Set α), μ sᶜ = 0 ↔ s = univ) ↔ ∀ (a : α), ¬μ {a} = 0

Tactic:
refine ⟨fun h a ha ↦ by simpa [ha] using (h {a}ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩

Result:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ s = univ

case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0

Proof state:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0

Tactic:
rintro rfl

Result:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
⊢ μ univᶜ = 0

Proof state:
case refine_1.intro
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
a : α
ha : a ∈ sᶜ
⊢ False

Tactic:
exact h _ <| measure_mono_null (singleton_subset_iff.2 ha) hs

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Module.lean
/--
If `M` is a finitely presented module over a local ring `(R, 𝔪)` such that `m ⊗ M → M` is
injective, then every generating family contains a basis.
-/
lemma exists_basis_of_span_of_maximalIdeal_rTensor_injective [Module.FinitePresentation R M]
    (H : Function.Injective ((𝔪).subtype.rTensor M))
    {ι : Type u} (v : ι → M) (hv : Submodule.span R (Set.range v) = ⊤) :
    ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ i, b i = v (a i)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

Tactic:
exact Set.Subset.trans this (Submodule.span_subset_span _ _ _)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this✝ : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
this : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
κ : Type u
a : κ → ι
ha : Function.Injective a
hsp : Submodule.span k (Set.range ((⇑((TensorProduct.mk R k M) 1) ∘ v) ∘ a)) = ⊤
hli : LinearIndependent k ((⇑((TensorProduct.mk R k M) 1) ∘ v) ∘ a)
b : Basis κ R M
hb : ∀ (i : κ), b i = (v ∘ a) i
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
use κ, a, b, hb

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem single_dotProduct (x : α) (i : m) : Pi.single i x ⬝ᵥ v = x * v i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ Pi.single i x ⬝ᵥ v = x * v i

Tactic:
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ Pi.single i x ⬝ᵥ v = x * v i

Tactic:
have : ∀ j ≠ i, Pi.single (f := fun _ => α) i x j * v j = 0 := fun j hij => by
  simp [Pi.single_eq_of_ne hij]

Result:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ Pi.single i x ⬝ᵥ v = x * v i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ Pi.single i x j * v j = 0

Tactic:
simp [Pi.single_eq_of_ne hij]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem probability (n : ℕ) (x : I) : (∑ k : Fin (n + 1), bernstein n k x) = 1

Proof state:
n : ℕ
x : ↑I
this : (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = (Polynomial.aeval ↑x) 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Tactic:
simp? [map_sum, Finset.sum_range] at this says
  simp only [Finset.sum_range, map_sum, Polynomial.coe_aeval_eq_eval, Polynomial.eval_one] at this

Result:
n : ℕ
x : ↑I
this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Proof state:
n : ℕ
x : ↑I
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Tactic:
have := bernsteinPolynomial.sum ℝ n

Result:
n : ℕ
x : ↑I
this : ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν = 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Proof state:
n : ℕ
x : ↑I
this : ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν = 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Tactic:
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this

Result:
n : ℕ
x : ↑I
this : (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = (Polynomial.aeval ↑x) 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Proof state:
n : ℕ
x : ↑I
this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Tactic:
exact this

Result:
no goals

Proof state:
n : ℕ
x : ↑I
this : (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = (Polynomial.aeval ↑x) 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1

Tactic:
simp only [Finset.sum_range, map_sum, Polynomial.coe_aeval_eq_eval, Polynomial.eval_one] at this

Result:
n : ℕ
x : ↑I
this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1
⊢ ∑ k : Fin (n + 1), (bernstein n ↑k) x = 1
-- Mathlib/Order/DirectedInverseSystem.lean
theorem induction₂ {C : DirectLimit F f → DirectLimit F f → Prop}
    (ih : ∀ i x y, C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧) (x y : DirectLimit F f) : C x y

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
x y : DirectLimit F f
⊢ C x y

Tactic:
obtain ⟨_, _, _, rfl, rfl⟩ := exists_eq_mk₂ f x y

Result:
case intro.intro.intro.intro
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
w✝² : ι
w✝¹ w✝ : F w✝²
⊢ C ⟦⟨w✝², w✝¹⟩⟧ ⟦⟨w✝², w✝⟩⟧

Proof state:
case intro.intro.intro.intro
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
w✝² : ι
w✝¹ w✝ : F w✝²
⊢ C ⟦⟨w✝², w✝¹⟩⟧ ⟦⟨w✝², w✝⟩⟧

Tactic:
apply ih

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_convergent_zero_of_isBigO {b : ℝ} {f : ℝ → ℝ}
    (hfc : AEStronglyMeasurable f <| volume.restrict (Ioi 0))
    (hf :  f =O[𝓝[>] 0] (· ^ (-b))) {s : ℝ} (hs : b < s) :
    ∃ c : ℝ, 0 < c ∧ IntegrableOn (fun t : ℝ => t ^ (s - 1) * f t) (Ioc 0 c)

Proof state:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x => x ^ (-b)
s : ℝ
hs : b < s
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
obtain ⟨d, _, hd'⟩ := hf.exists_pos

Result:
case intro.intro
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x => x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : IsBigOWith d (𝓝[>] 0) f fun x => x ^ (-b)
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume

Proof state:
case intro.intro
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x => x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : IsBigOWith d (𝓝[>] 0) f fun x => x ^ (-b)
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
simp_rw [IsBigOWith, eventually_nhdsWithin_iff, Metric.eventually_nhds_iff, gt_iff_lt] at hd'

Result:
case intro.intro
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x => x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : ∃ ε, 0 < ε ∧ ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume

Proof state:
case intro.intro
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x => x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : ∃ ε, 0 < ε ∧ ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
obtain ⟨ε, hε, hε'⟩ := hd'

Result:
case intro.intro.intro.intro
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x => x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
theorem hasEqualizer_of_common_retraction [HasCoreflexiveEqualizers C] {A B : C} {f g : A ⟶ B}
    (r : B ⟶ A) (fr : f ≫ r = 𝟙 _) (gr : g ≫ r = 𝟙 _) : HasEqualizer f g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
this : IsCoreflexivePair f g := IsCoreflexivePair.mk' r fr gr
⊢ HasEqualizer f g

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
⊢ HasEqualizer f g

Tactic:
letI := IsCoreflexivePair.mk' r fr gr

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
this : IsCoreflexivePair f g := IsCoreflexivePair.mk' r fr gr
⊢ HasEqualizer f g
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem transfer_transfer (hp) {K : SimpleGraph V} (hp') :
    (p.transfer H hp).transfer K hp' = p.transfer K (p.edges_transfer hp ▸ hp')

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih :
  ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet) (hp' : ∀ e ∈ (p✝.transfer H hp).edges, e ∈ K.edgeSet),
    (p✝.transfer H hp).transfer K hp' = p✝.transfer K ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
hp' : ∀ e ∈ ((cons h✝ p✝).transfer H hp).edges, e ∈ K.edgeSet
⊢ (p✝.transfer H ⋯).transfer K ⋯ = p✝.transfer K ⋯

Tactic:
apply ih

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
K : SimpleGraph V
hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯

Tactic:
induction p with
| nil => simp
| cons _ _ ih =>
  simp only [Walk.transfer, cons.injEq, heq_eq_eq, true_and]
  apply ih

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih :
  ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet) (hp' : ∀ e ∈ (p✝.transfer H hp).edges, e ∈ K.edgeSet),
    (p✝.transfer H hp).transfer K hp' = p✝.transfer K ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
hp' : ∀ e ∈ ((cons h✝ p✝).transfer H hp).edges, e ∈ K.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).transfer K hp' = (cons h✝ p✝).transfer K ⋯

Tactic:
simp only [Walk.transfer, cons.injEq, heq_eq_eq, true_and]

Result:
case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih :
  ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet) (hp' : ∀ e ∈ (p✝.transfer H hp).edges, e ∈ K.edgeSet),
    (p✝.transfer H hp).transfer K hp' = p✝.transfer K ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
hp' : ∀ e ∈ ((cons h✝ p✝).transfer H hp).edges, e ∈ K.edgeSet
⊢ (p✝.transfer H ⋯).transfer K ⋯ = p✝.transfer K ⋯

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u✝ : V
hp : ∀ e ∈ nil.edges, e ∈ H.edgeSet
hp' : ∀ e ∈ (nil.transfer H hp).edges, e ∈ K.edgeSet
⊢ (nil.transfer H hp).transfer K hp' = nil.transfer K ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Partition.lean
@[simp] lemma partition_one_parts (p : Partition 1) : p.parts = {1}

Proof state:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts = {1}

Tactic:
have h' : card p.parts = 1 := by simpa using (congrArg sum h.symm).trans p.parts_sum

Result:
p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
⊢ p.parts = {1}

Proof state:
p : Partition 1
⊢ p.parts = {1}

Tactic:
have h : p.parts = replicate (card p.parts) 1 := eq_replicate_card.2 fun x hx =>
  ((le_sum_of_mem hx).trans_eq p.parts_sum).antisymm (p.parts_pos hx)

Result:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts = {1}

Proof state:
p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
⊢ p.parts = {1}

Tactic:
rw [h, h', replicate_one]

Result:
no goals

Proof state:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts.card = 1

Tactic:
simpa using (congrArg sum h.symm).trans p.parts_sum

Result:
no goals