harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem ext {σ τ : p.Gal} (h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x) : σ = τ

Proof state:
F : Type u_1
inst✝ : Field F
p : F[X]
σ τ : p.Gal
h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x
⊢ σ = τ

Tactic:
refine
  AlgEquiv.ext fun x =>
    (AlgHom.mem_equalizer σ.toAlgHom τ.toAlgHom x).mp
      ((SetLike.ext_iff.mp ?_ x).mpr Algebra.mem_top)

Result:
F : Type u_1
inst✝ : Field F
p : F[X]
σ τ : p.Gal
h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x
x : p.SplittingField
⊢ AlgHom.equalizer ↑σ ↑τ = ⊤

Proof state:
F : Type u_1
inst✝ : Field F
p : F[X]
σ τ : p.Gal
h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x
x : p.SplittingField
⊢ AlgHom.equalizer ↑σ ↑τ = ⊤

Tactic:
rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem exists_mem (ha : a ∈ s) : ∃ t ∈ P.parts, a ∈ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ P.parts.sup id
⊢ ∃ t ∈ P.parts, a ∈ t

Tactic:
exact mem_sup.1 ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ t ∈ P.parts, a ∈ t

Tactic:
simp_rw [← P.sup_parts] at ha

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ P.parts.sup id
⊢ ∃ t ∈ P.parts, a ∈ t
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tendsto_card_div_pow₂ (hs₁ : IsBounded s)
    (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) {x y : ℝ} (hx : 0 < x) (hy : x ≤ y) :
    Nat.card ↑(s ∩ x⁻¹ • L) ≤ Nat.card ↑(s ∩ y⁻¹ • L)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ Nat.card ↑(x • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
refine Nat.card_mono ?_ ?_

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ (y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).Finite

case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ x • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ⊆ y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ (y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).Finite

Tactic:
exact ZSpan.setFinite_inter _ (IsBounded.smul₀ hs₁ y)

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ x • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ⊆ y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
exact Set.inter_subset_inter_left _ <| hs₄ hx hy

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ y⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
rw [Nat.card_congr (tendsto_card_div_pow₁ s hx.ne'),
    Nat.card_congr (tendsto_card_div_pow₁ s (hx.trans_le hy).ne')]

Result:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ Nat.card ↑(x • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem comap_normalizer_eq_of_surjective (H : Subgroup G) {f : N →* G}
    (hf : Function.Surjective f) : H.normalizer.comap f = (H.comap f).normalizer :=
  le_antisymm (le_normalizer_comap f)
    (by
      intro x hx
      simp only [mem_comap, mem_normalizer_iff] at *
      intro n
      rcases hf n with ⟨y, rfl⟩
      simp [hx y])

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
⊢ ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H

Tactic:
intro n

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
n : G
⊢ n ∈ H ↔ f x * n * (f x)⁻¹ ∈ H

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
n : G
⊢ n ∈ H ↔ f x * n * (f x)⁻¹ ∈ H

Tactic:
rcases hf n with ⟨y, rfl⟩

Result:
case intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
y : N
⊢ f y ∈ H ↔ f x * f y * (f x)⁻¹ ∈ H

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
⊢ (comap f H).normalizer ≤ comap f H.normalizer

Tactic:
intro x hx

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : x ∈ (comap f H).normalizer
⊢ x ∈ comap f H.normalizer

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
y : N
⊢ f y ∈ H ↔ f x * f y * (f x)⁻¹ ∈ H

Tactic:
simp [hx y]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : x ∈ (comap f H).normalizer
⊢ x ∈ comap f H.normalizer

Tactic:
simp only [mem_comap, mem_normalizer_iff] at *

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Surjective ⇑f
x : N
hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
⊢ ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
lemma _root_.HasCompactSupport.enorm_le_lintegral_Ici_deriv
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    {f : ℝ → F} (hf : ContDiff ℝ 1 f) (h'f : HasCompactSupport f) (x : ℝ) :
    ‖f x‖ₑ ≤ ∫⁻ y in Iic x, ‖deriv f y‖ₑ

Proof state:
case h.e'_4.h.e'_4.h
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := ⇑I ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
y : ℝ
⊢ ‖deriv f y‖ₑ = ‖I (deriv f y)‖ₑ

Tactic:
simp [I]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_eq_allOnes_iff {x y : BitVec w} :
    x &&& y = allOnes w ↔ x = allOnes w ∧ y = allOnes w

Proof state:
case mp
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
⊢ x = allOnes w ∧ y = allOnes w

Tactic:
constructor

Result:
case mp.left
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
⊢ x = allOnes w

case mp.right
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
⊢ y = allOnes w

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ x = allOnes w ∧ y = allOnes w → x &&& y = allOnes w

Tactic:
intro h

Result:
case mpr
w : Nat
x y : BitVec w
h : x = allOnes w ∧ y = allOnes w
⊢ x &&& y = allOnes w

Proof state:
case mp.right
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
⊢ y = allOnes w

Tactic:
ext i ih

Result:
case mp.right.pred
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
i : Nat
ih : i < w
⊢ y.getLsbD i = (allOnes w).getLsbD i

Proof state:
case mp.right.pred
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
i : Nat
ih : i < w
this : (x &&& y).getLsbD i = (allOnes w).getLsbD i
⊢ y.getLsbD i = (allOnes w).getLsbD i

Tactic:
simp only [getLsbD_and, getLsbD_allOnes, ih, decide_true, Bool.and_eq_true] at this

Result:
case mp.right.pred
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
i : Nat
ih : i < w
this : x.getLsbD i = true ∧ y.getLsbD i = true
⊢ y.getLsbD i = (allOnes w).getLsbD i

Proof state:
case mp.right.pred
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
i : Nat
ih : i < w
⊢ y.getLsbD i = (allOnes w).getLsbD i

Tactic:
have := BitVec.eq_of_getLsbD_eq_iff.mp h i ih

Result:
case mp.right.pred
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
i : Nat
ih : i < w
this : (x &&& y).getLsbD i = (allOnes w).getLsbD i
⊢ y.getLsbD i = (allOnes w).getLsbD i

Proof state:
w : Nat
x y : BitVec w
⊢ x &&& y = allOnes w ↔ x = allOnes w ∧ y = allOnes w

Tactic:
constructor

Result:
case mp
w : Nat
x y : BitVec w
⊢ x &&& y = allOnes w → x = allOnes w ∧ y = allOnes w

case mpr
w : Nat
x y : BitVec w
⊢ x = allOnes w ∧ y = allOnes w → x &&& y = allOnes w

Proof state:
case mp
w : Nat
x y : BitVec w
⊢ x &&& y = allOnes w → x = allOnes w ∧ y = allOnes w

Tactic:
intro h

Result:
case mp
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
⊢ x = allOnes w ∧ y = allOnes w

Proof state:
case mp.right.pred
w : Nat
x y : BitVec w
h : x &&& y = allOnes w
i : Nat
ih : i < w
this : x.getLsbD i = true ∧ y.getLsbD i = true
⊢ y.getLsbD i = (allOnes w).getLsbD i

Tactic:
simp [this, ih]

Result:
no goals

Proof state:
case mpr
w : Nat
x y : BitVec w
h : x = allOnes w ∧ y = allOnes w
⊢ x &&& y = allOnes w

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.map_dest {α β : TypeVec n} (g : (α ::: P.M α) ⟹ (β ::: P.M β)) (x : P.M α)
    (h : ∀ x : P.M α, lastFun g x = (dropFun g <$$> x : P.M β)) :
    g <$$> M.dest P x = M.dest P (dropFun g <$$> x)

Proof state:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x => dropFun g <$$> x

Tactic:
ext1

Result:
case e_a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
x✝ : (α ::: P.M α).last
⊢ lastFun g x✝ = dropFun g <$$> x✝

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ dropFun g = dropFun (dropFun g ::: fun x => dropFun g <$$> x)

Tactic:
simp

Result:
no goals

Proof state:
case e_a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
x✝ : (α ::: P.M α).last
⊢ lastFun g x✝ = dropFun g <$$> x✝

Tactic:
apply h

Result:
no goals

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x

Tactic:
congr

Result:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g = (dropFun g ::: fun x => dropFun g <$$> x)

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)

Tactic:
rw [M.dest_map]

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x

Proof state:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g = (dropFun g ::: fun x => dropFun g <$$> x)

Tactic:
apply eq_of_drop_last_eq (by simp)

Result:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = lastFun (dropFun g ::: fun x => dropFun g <$$> x)

Proof state:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = lastFun (dropFun g ::: fun x => dropFun g <$$> x)

Tactic:
simp only [lastFun_appendFun]

Result:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x => dropFun g <$$> x
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_foldr (b o : Ordinal) : (CNF b o).foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 = o

Proof state:
case refine_2
b o : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}),
    o ≠ 0 →
      foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
        foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
intro o ho IH

Result:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Proof state:
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
refine CNFRec b ?_ ?_ o

Result:
case refine_1
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b 0) = 0

case refine_2
b o : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}),
    o ≠ 0 →
      foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
        foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Proof state:
case refine_1
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b 0) = 0

Tactic:
rw [CNF_zero, foldr_nil]

Result:
no goals

Proof state:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
rw [CNF_ne_zero ho, foldr_cons, IH, div_add_mod]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem sum_ite_self_eq [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (f.sum fun x v => ite (a = x) v 0) = f a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v => if a = x then v else 0) = f a

Tactic:
convert f.sum_ite_eq a fun _ => id

Result:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ f a = if a ∈ f.support then id (f a) else 0

Proof state:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ f a = if a ∈ f.support then id (f a) else 0

Tactic:
simp [ite_eq_right_iff.2 Eq.symm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v => if a = x then v else 0) = f a

Tactic:
classical
  convert f.sum_ite_eq a fun _ => id
  simp [ite_eq_right_iff.2 Eq.symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_allOnes : (allOnes w).toInt = if 0 < w then -1 else 0

Proof state:
case pos
w : Nat
h : w = 0
⊢ (allOnes w).toInt = if 0 < w then -1 else 0

Tactic:
subst h

Result:
case pos

⊢ (allOnes 0).toInt = if 0 < 0 then -1 else 0

Proof state:
case neg
w : Nat
h : ¬w = 0
this : 1 < 2 ^ w
⊢ (allOnes w).toInt = if 0 < w then -1 else 0

Tactic:
simp [BitVec.toInt]

Result:
case neg
w : Nat
h : ¬w = 0
this : 1 < 2 ^ w
⊢ (if 2 * (2 ^ w - 1) < 2 ^ w then ↑(2 ^ w - 1) else ↑(2 ^ w - 1) - ↑(2 ^ w)) = if 0 < w then -1 else 0

Proof state:
case pos

⊢ (allOnes 0).toInt = if 0 < 0 then -1 else 0

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
⊢ (allOnes w).toInt = if 0 < w then -1 else 0

Tactic:
by_cases h : w = 0

Result:
case pos
w : Nat
h : w = 0
⊢ (allOnes w).toInt = if 0 < w then -1 else 0

case neg
w : Nat
h : ¬w = 0
⊢ (allOnes w).toInt = if 0 < w then -1 else 0

Proof state:
w : Nat
h : ¬w = 0
⊢ 1 < 2 ^ w

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
w : Nat
h : ¬w = 0
this : 1 < 2 ^ w
⊢ (if 2 * (2 ^ w - 1) < 2 ^ w then ↑(2 ^ w - 1) else ↑(2 ^ w - 1) - ↑(2 ^ w)) = if 0 < w then -1 else 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
h : ¬w = 0
⊢ (allOnes w).toInt = if 0 < w then -1 else 0

Tactic:
have : 1 < 2 ^ w := by simp [h]

Result:
case neg
w : Nat
h : ¬w = 0
this : 1 < 2 ^ w
⊢ (allOnes w).toInt = if 0 < w then -1 else 0
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_id_of_mono {x : SimplexCategory} (i : x ⟶ x) [Mono i] : i = 𝟙 _

Proof state:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Mono i

Tactic:
infer_instance

Result:
no goals

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ IsIso i

Tactic:
apply isIso_of_bijective

Result:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Function.Bijective (Hom.toOrderHom i).toFun

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
this : IsIso i
⊢ i = 𝟙 x

Tactic:
apply eq_id_of_isIso

Result:
no goals

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ i = 𝟙 x

Tactic:
suffices IsIso i by
  apply eq_id_of_isIso

Result:
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ IsIso i

Proof state:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Function.Bijective ⇑(Hom.toOrderHom i)

Tactic:
rw [Fintype.bijective_iff_injective_and_card i.toOrderHom, ← mono_iff_injective,
  eq_self_iff_true, and_true]

Result:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Mono i

Proof state:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Function.Bijective (Hom.toOrderHom i).toFun

Tactic:
dsimp

Result:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Function.Bijective ⇑(Hom.toOrderHom i)
-- Mathlib/CategoryTheory/Subpresheaf/Basic.lean
theorem eq_top_iff_isIso : G = ⊤ ↔ IsIso G.ι

Proof state:
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ G.obj U ↔ x ∈ ⊤.obj U

Tactic:
apply (iff_of_eq (iff_true _)).mpr

Result:
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ G.obj U

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ G = ⊤ → IsIso G.ι

Tactic:
rintro rfl

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
⊢ IsIso ⊤.ι

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
⊢ G = ⊤

Tactic:
ext U x

Result:
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ G.obj U ↔ x ∈ ⊤.obj U

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ IsIso G.ι → G = ⊤

Tactic:
intro H

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
⊢ G = ⊤

Proof state:
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ G.obj U

Tactic:
rw [← IsIso.inv_hom_id_apply (G.ι.app U) x]

Result:
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
U : Cᵒᵖ
x : F.obj U
⊢ (ConcreteCategory.hom (G.ι.app U)) ((ConcreteCategory.hom (inv (G.ι.app U))) x) ∈ G.obj U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ G = ⊤ ↔ IsIso G.ι

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ G = ⊤ → IsIso G.ι

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ IsIso G.ι → G = ⊤

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
⊢ IsIso ⊤.ι

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
H : IsIso G.ι
U : Cᵒᵖ
x : F.obj U
⊢ (ConcreteCategory.hom (G.ι.app U)) ((ConcreteCategory.hom (inv (G.ι.app U))) x) ∈ G.obj U

Tactic:
exact ((inv (G.ι.app U)) x).2

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDerivWithin_comp_of_eventually_mem {t : Set F}
    (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContDiffWithinAt 𝕜 n f s x)
    (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hxs : x ∈ s) (hst : ∀ᶠ y in 𝓝[s] x, f y ∈ t)
    {i : ℕ} (hi : i ≤ n) :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : WithTop ℕ∞
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
⊢ ∃ u,
    x ∈ u ∧
      IsOpen u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))

Tactic:
have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets,
    HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
  hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : WithTop ℕ∞
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) u
⊢ ∃ u,
    x ∈ u ∧
      IsOpen u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
-- Mathlib/Order/Hom/Basic.lean
theorem OrderIso.isMax_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
    IsMax (f x) ↔ IsMax x

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f x) ↔ IsMax x

Tactic:
refine ⟨f.strictMono.isMax_of_apply, ?_⟩

Result:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax x → IsMax (f x)

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f.symm (f x)) → IsMax (f x)

Tactic:
exact f.symm.strictMono.isMax_of_apply

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax x → IsMax (f x)

Tactic:
conv_lhs => rw [← f.symm_apply_apply x]

Result:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f.symm (f x)) → IsMax (f x)