harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftMonoidWithZeroHom_injective [Nontrivial R] (φ : R[X] →*₀ G₀) (hφ : Function.Injective φ)
    (hφ' : R[X]⁰ ≤ G₀⁰.comap φ := nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ hφ) :
    Function.Injective (liftMonoidWithZeroHom φ hφ')

Proof state:
case ofFractionRing.ofFractionRing.H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Tactic:
congr 1

Result:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ Localization.mk a.1 a.2 = Localization.mk a'.1 a'.2

Proof state:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ ↑(a'.1, a'.2).2 * (a.1, a.2).1 = ↑(a.1, a.2).2 * (a'.1, a'.2).1

Tactic:
have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h

Result:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
this : φ a.1 * φ ↑a'.2 = φ a'.1 * φ ↑a.2
⊢ ↑(a'.1, a'.2).2 * (a.1, a.2).1 = ↑(a.1, a.2).2 * (a'.1, a'.2).1

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_1
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ φ ↑a.2 ≠ 0

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ φ ↑a'.2 ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ map Subtype.val { toList := toList✝ }.attach = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
⊢ map Subtype.val l.attach = l

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ map Subtype.val { toList := toList✝ }.attach = { toList := toList✝ }
-- Mathlib/Combinatorics/Colex.lean
lemma isInitSeg_initSeg : IsInitSeg (initSeg s) #s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
⊢ IsInitSeg (initSeg s) #s

Tactic:
refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩

Result:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ : { ofColex := t₂ } < { ofColex := t₁ } ∧ #t₂ = #s
⊢ { ofColex := t₂ } ≤ { ofColex := s }

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : #s = #t₁ ∧ { ofColex := t₁ } ≤ { ofColex := s }
ht₂ : { ofColex := t₂ } < { ofColex := t₁ } ∧ #t₂ = #s
⊢ { ofColex := t₂ } ≤ { ofColex := s }

Tactic:
exact ht₂.1.le.trans ht₁.2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : t₁ ∈ initSeg s
ht₂ : { ofColex := t₂ } < { ofColex := t₁ } ∧ #t₂ = #s
⊢ { ofColex := t₂ } ≤ { ofColex := s }

Tactic:
rw [mem_initSeg] at ht₁

Result:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : #s = #t₁ ∧ { ofColex := t₁ } ≤ { ofColex := s }
ht₂ : { ofColex := t₂ } < { ofColex := t₁ } ∧ #t₂ = #s
⊢ { ofColex := t₂ } ≤ { ofColex := s }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
    (replicate n a).max? = some a

Proof state:
α : Type u_1
inst✝ : Max α
n : Nat
a : α
w : max a a = a
h : 0 < n
⊢ (replicate n a).max? = some a

Tactic:
simp [max?_replicate, Nat.ne_of_gt h, w]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generateFrom_generatePiSystem_eq {g : Set (Set α)} :
    generateFrom (generatePiSystem g) = generateFrom g

Proof state:
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t

Tactic:
exact fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)

Result:
no goals

Proof state:
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) = generateFrom g

Tactic:
apply le_antisymm <;> apply generateFrom_le

Result:
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t

case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t

Proof state:
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t

Tactic:
exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_sup [Nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a

Tactic:
rw [iSup_sup_eq, iSup_const]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem spectralRadius_le_liminf_pow_nnnorm_pow_one_div (a : A) :
    spectralRadius 𝕜 a ≤ atTop.liminf fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop

Tactic:
by_cases h : ε = 0

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ε = 0
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop

case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹

Tactic:
rw [← ENNReal.inv_lt_inv, inv_one] at hε

Result:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l){h'} :
    get (insertMany m l) k' h' = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
h' : k' ∈ insertMany m l
⊢ get (insertMany m l) k' h' = v

Tactic:
simp_to_raw using Raw₀.Const.get_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hasse.lean
theorem hasse_prod : hasse (α × β) = hasse α □ hasse β

Proof state:
case Adj.h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (hasse (α × β)).Adj x y ↔ (hasse α □ hasse β).Adj x y

Tactic:
simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
  or_or_or_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
⊢ hasse (α × β) = hasse α □ hasse β

Tactic:
ext x y

Result:
case Adj.h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (hasse (α × β)).Adj x y ↔ (hasse α □ hasse β).Adj x y
-- Mathlib/Combinatorics/HalesJewett.lean
theorem vertical_apply {α ι ι'} (v : ι → α) (l : Line α ι') (x : α) :
    l.vertical v x = Sum.elim v (l x)

Proof state:
case h
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ ↑(vertical v l) x i = Sum.elim v (↑l x) i

Tactic:
cases i <;> rfl

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
⊢ ↑(vertical v l) x = Sum.elim v (↑l x)

Tactic:
funext i

Result:
case h
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
i : ι ⊕ ι'
⊢ ↑(vertical v l) x i = Sum.elim v (↑l x) i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a)

Proof state:
m : Type u_1 → Type u_2
α ε β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
f : α → ExceptT ε m β
⊢ (ExceptT.lift x >>= f).run = do
    let a ← x
    (f a).run

Tactic:
simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_succ (o : Ordinal) : card (succ o) = card o + 1

Proof state:
o : Ordinal.{u_1}
⊢ (succ o).card = o.card + 1

Tactic:
simp only [← add_one_eq_succ, card_add, card_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_map' (f : α₁ → α₂) (g : α₂ → β → β) (l : Array α₁) (init : β) (w : start = l.size) :
    (l.map f).foldr g init start 0 = l.foldr (fun x y => g (f x) y) init

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
init : β
toList✝ : List α₁
⊢ foldr g init (map f { toList := toList✝ }) { toList := toList✝ }.size =
    foldr (fun x y => g (f x) y) init { toList := toList✝ }

Tactic:
simp [List.foldr_map]

Result:
no goals

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
l : Array α₁
init : β
⊢ foldr g init (map f l) l.size = foldr (fun x y => g (f x) y) init l

Tactic:
cases l

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
init : β
toList✝ : List α₁
⊢ foldr g init (map f { toList := toList✝ }) { toList := toList✝ }.size =
    foldr (fun x y => g (f x) y) init { toList := toList✝ }

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
start : Nat
f : α₁ → α₂
g : α₂ → β → β
l : Array α₁
init : β
w : start = l.size
⊢ foldr g init (map f l) start = foldr (fun x y => g (f x) y) init l

Tactic:
subst w

Result:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
l : Array α₁
init : β
⊢ foldr g init (map f l) l.size = foldr (fun x y => g (f x) y) init l
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_xor : ∀ m n : Num, ↑(m ^^^ n) = (↑m ^^^ ↑n : ℕ)

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor (PosNum.bit b✝ n✝) = bit (a✝ != b✝) (m✝.lxor n✝)

Tactic:
cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor (PosNum.bit b✝ n✝) = bit (a✝ != b✝) (m✝.lxor n✝)

Tactic:
try cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)

Proof state:
⊢ ∀ (m n : Num), ↑(m ^^^ n) = ↑m ^^^ ↑n

Tactic:
apply castNum_eq_bitwise PosNum.lxor <;> intros <;> (try cases_type* Bool) <;> rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
theorem extremePoints_convexHull_subset : (convexHull 𝕜 A).extremePoints 𝕜 ⊆ A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hx : x ∈ extremePoints 𝕜 ((convexHull 𝕜) A)
⊢ x ∈ A

Tactic:
rw [(convex_convexHull 𝕜 _).mem_extremePoints_iff_convex_diff] at hx

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})
⊢ x ∈ A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})
h : x ∉ A
⊢ False

Tactic:
exact (convexHull_min (subset_diff.2 ⟨subset_convexHull 𝕜 _, disjoint_singleton_right.2 h⟩) hx.2
  hx.1).2 rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
⊢ extremePoints 𝕜 ((convexHull 𝕜) A) ⊆ A

Tactic:
rintro x hx

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hx : x ∈ extremePoints 𝕜 ((convexHull 𝕜) A)
⊢ x ∈ A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})
⊢ x ∈ A

Tactic:
by_contra h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})
h : x ∉ A
⊢ False
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem wideCoequalizer.π_desc [Nonempty J] {W : C} (k : Y ⟶ W)
    (h : ∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k) :
    wideCoequalizer.π f ≫ wideCoequalizer.desc k h = k

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝¹ : HasWideCoequalizer f
inst✝ : Nonempty J
W : C
k : Y ⟶ W
h : ∀ (j₁ j₂ : J), f j₁ ≫ k = f j₂ ≫ k
⊢ π f ≫ desc k h = k

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem principal_le_iff {s : Set α} {f : Filter α} : 𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V

Proof state:
α : Type u
s : Set α
f : Filter α
⊢ 𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V

Tactic:
simp_rw [le_def, mem_principal]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_ceil_atBot : Tendsto (ceil : α → ℤ) atBot atBot :=
  ceil_mono.tendsto_atBot_atBot fun b =>
    ⟨(b - 1 : ℤ), by rw [ceil_intCast]; exact (sub_one_lt _).le⟩

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ ⌈↑(b - 1)⌉ ≤ b

Tactic:
rw [ceil_intCast]

Result:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b - 1 ≤ b

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b - 1 ≤ b

Tactic:
exact (sub_one_lt _).le

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem mulLeft_mul [SMulCommClass R A A] (a b : A) :
    mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b : A
⊢ mulLeft R (a * b) = mulLeft R a ∘ₗ mulLeft R b

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b x✝ : A
⊢ (mulLeft R (a * b)) x✝ = (mulLeft R a ∘ₗ mulLeft R b) x✝

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b x✝ : A
⊢ (mulLeft R (a * b)) x✝ = (mulLeft R a ∘ₗ mulLeft R b) x✝

Tactic:
simp only [mulLeft_apply, comp_apply, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) :
    logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)

Proof state:
b : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)

Tactic:
induction' s using Finset.induction_on with a s ha ih

Result:
case empty
b : ℝ
α : Type u_1
f : α → ℝ
hf : ∀ x ∈ ∅, f x ≠ 0
⊢ logb b (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, logb b (f i)

case insert
b : ℝ
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
hf : ∀ x ∈ insert a s, f x ≠ 0
⊢ logb b (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, logb b (f i)

Proof state:
case insert
b : ℝ
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
hf : ∀ x ∈ insert a s, f x ≠ 0
⊢ logb b (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, logb b (f i)

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hf

Result:
case insert
b : ℝ
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
hf : f a ≠ 0 ∧ ∀ a ∈ s, f a ≠ 0
⊢ logb b (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, logb b (f i)

Proof state:
case empty
b : ℝ
α : Type u_1
f : α → ℝ
hf : ∀ x ∈ ∅, f x ≠ 0
⊢ logb b (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, logb b (f i)

Tactic:
simp

Result:
no goals

Proof state:
case insert
b : ℝ
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)
hf : f a ≠ 0 ∧ ∀ a ∈ s, f a ≠ 0
⊢ logb b (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, logb b (f i)

Tactic:
simp [ha, ih hf.2, logb_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
/-- The moment generating function is analytic at every `t ∈ interior (integrableExpSet X μ)`. -/
lemma analyticAt_mgf (ht : t ∈ interior (integrableExpSet X μ)) :
    AnalyticAt ℝ (mgf X μ) t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (fun x => (complexMGF X μ ↑x).re) t

Tactic:
exact (analyticAt_complexMGF (by simp [ht])).re_ofReal

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (↑t).re ∈ interior (integrableExpSet X μ)

Tactic:
simp [ht]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (mgf X μ) t

Tactic:
rw [← re_complexMGF_ofReal']

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℝ (fun x => (complexMGF X μ ↑x).re) t
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_C (x : R) : (C x).roots = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
⊢ (C x).roots = 0

Tactic:
exact
if H : x = 0 then by rw [H, C_0, roots_zero]
else
Multiset.ext.mpr fun r => (by
rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)])

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
H : ¬x = 0
r : R
⊢ count r (C x).roots = count r 0

Tactic:
rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
⊢ (C x).roots = 0

Tactic:
classical exact
if H : x = 0 then by rw [H, C_0, roots_zero]
else
  Multiset.ext.mpr fun r => (by
    rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)])

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
H : x = 0
⊢ (C x).roots = 0

Tactic:
rw [H, C_0, roots_zero]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_id (n : ℕ) : (id : α → α)^[n] = id :=
  Nat.recOn n rfl fun n ihn ↦ by rw [iterate_succ, ihn, id_comp]

Proof state:
α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[n.succ] = id

Tactic:
rw [iterate_succ, ihn, id_comp]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem natCast_fin_two (n : ℕ) : (n : Matrix (Fin 2) (Fin 2) α) = !![↑n, 0; 0, ↑n]

Proof state:
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n = !![↑n, 0; 0, ↑n]

Tactic:
ext i j

Result:
case a
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 2
⊢ ↑n i j = !![↑n, 0; 0, ↑n] i j

Proof state:
case a
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 2
⊢ ↑n i j = !![↑n, 0; 0, ↑n] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
/-- An object in `Type u` is initial if and only if it is empty. -/
lemma initial_iff_empty (X : Type u) : Nonempty (IsInitial X) ↔ IsEmpty X

Proof state:
case mp
X : Type u
⊢ Nonempty (IsInitial X) → IsEmpty X

Tactic:
intro ⟨h⟩

Result:
case mp
X : Type u
h : IsInitial X
⊢ IsEmpty X

Proof state:
X : Type u
⊢ Nonempty (IsInitial X) ↔ IsEmpty X

Tactic:
constructor

Result:
case mp
X : Type u
⊢ Nonempty (IsInitial X) → IsEmpty X

case mpr
X : Type u
⊢ IsEmpty X → Nonempty (IsInitial X)

Proof state:
case mp
X : Type u
h : IsInitial X
⊢ IsEmpty X

Tactic:
exact Function.isEmpty (IsInitial.to h PEmpty)

Result:
no goals

Proof state:
case mpr
X : Type u
h : IsEmpty X
⊢ Nonempty (IsInitial X)

Tactic:
exact ⟨IsInitial.ofIso Types.isInitialPunit <| Equiv.toIso <| Equiv.equivOfIsEmpty PEmpty X⟩

Result:
no goals

Proof state:
case mpr
X : Type u
⊢ IsEmpty X → Nonempty (IsInitial X)

Tactic:
intro h

Result:
case mpr
X : Type u
h : IsEmpty X
⊢ Nonempty (IsInitial X)
-- Mathlib/Data/Nat/Bitwise.lean
theorem xor_eq_zero {n m : ℕ} : n ^^^ m = 0 ↔ n = m

Proof state:
n m : ℕ
⊢ n ^^^ m = 0 ↔ n = m

Tactic:
rw [← Nat.xor_self n, xor_right_inj, eq_comm]

Result:
no goals