harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Finite/Lattice.lean
lemma map_finite_biInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [InfTopHomClass F α β] {s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) :
    f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : InfTopHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (⨅ a ∈ s, g a) = ⨅ a ∈ s, f (g a)
⊢ f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : InfTopHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (hs.toFinset.inf g) = hs.toFinset.inf (⇑f ∘ g)
⊢ f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Tactic:
simp only [Finset.inf_eq_iInf, hs.mem_toFinset, comp_apply] at this

Result:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : InfTopHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (⨅ a ∈ s, g a) = ⨅ a ∈ s, f (g a)
⊢ f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : InfTopHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
⊢ f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Tactic:
have := map_finset_inf f hs.toFinset g

Result:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : InfTopHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (hs.toFinset.inf g) = hs.toFinset.inf (⇑f ∘ g)
⊢ f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)
-- Mathlib/SetTheory/Game/PGame.lean
theorem rightMoves_add_cases {x y : PGame} (k) {P : (x + y).RightMoves → Prop}
    (hl : ∀ j, P <| toRightMovesAdd (Sum.inl j)) (hr : ∀ j, P <| toRightMovesAdd (Sum.inr j)) :
    P k

Proof state:
case inr
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
i : y.RightMoves
⊢ P (toRightMovesAdd (Sum.inr i))

Tactic:
exact hr i

Result:
no goals

Proof state:
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
⊢ P (toRightMovesAdd (toRightMovesAdd.symm k))

Tactic:
rcases toRightMovesAdd.symm k with i | i

Result:
case inl
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
i : x.RightMoves
⊢ P (toRightMovesAdd (Sum.inl i))

case inr
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
i : y.RightMoves
⊢ P (toRightMovesAdd (Sum.inr i))

Proof state:
case inl
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
i : x.RightMoves
⊢ P (toRightMovesAdd (Sum.inl i))

Tactic:
exact hl i

Result:
no goals

Proof state:
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
⊢ P k

Tactic:
rw [← toRightMovesAdd.apply_symm_apply k]

Result:
x y : PGame
k : (x + y).RightMoves
P : (x + y).RightMoves → Prop
hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))
hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))
⊢ P (toRightMovesAdd (toRightMovesAdd.symm k))
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem IsGLB.mul_left {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) :
    IsGLB ((fun b => a * b) '' s) (a * b)

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b => a * b) '' s) (a * b)

Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl)

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b => a * b) '' s) (a * b)

case inr
α : Type u_2
inst✝ : LinearOrderedSemifield α
b : α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b => 0 * b) '' s) (0 * b)

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedSemifield α
b : α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a => 0) '' s) 0

Tactic:
rw [hs.nonempty.image_const]

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedSemifield α
b : α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b => a * b) '' s) (a * b)

Tactic:
exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedSemifield α
b : α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0

Tactic:
exact isGLB_singleton

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedSemifield α
b : α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b => 0 * b) '' s) (0 * b)

Tactic:
simp_rw [zero_mul]

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedSemifield α
b : α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a => 0) '' s) 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_le_size (p : α → Bool) {xs : Array α} : xs.findIdx p ≤ xs.size

Proof state:
case pos
α : Type u_1
p : α → Bool
xs : Array α
e : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.size

Tactic:
exact Nat.le_of_lt (findIdx_lt_size_of_exists e)

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
xs : Array α
e : ¬∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.size

Tactic:
simp at e

Result:
case neg
α : Type u_1
p : α → Bool
xs : Array α
e : ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p xs ≤ xs.size

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
⊢ findIdx p xs ≤ xs.size

Tactic:
by_cases e : ∃ x ∈ xs, p x

Result:
case pos
α : Type u_1
p : α → Bool
xs : Array α
e : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.size

case neg
α : Type u_1
p : α → Bool
xs : Array α
e : ¬∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs ≤ xs.size

Proof state:
case neg
α : Type u_1
p : α → Bool
xs : Array α
e : ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p xs ≤ xs.size

Tactic:
exact Nat.le_of_eq (findIdx_eq_size.mpr e)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem mem_cthickening_of_dist_le {α : Type*} [PseudoMetricSpace α] (x y : α) (δ : ℝ) (E : Set α)
    (h : y ∈ E) (h' : dist x y ≤ δ) : x ∈ cthickening δ E

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ

Tactic:
exact ENNReal.ofReal_le_ofReal h'

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ edist x y ≤ ENNReal.ofReal δ

Tactic:
rw [edist_dist]

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ x ∈ cthickening δ E

Tactic:
apply mem_cthickening_of_edist_le x y δ E h

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ edist x y ≤ ENNReal.ofReal δ
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (P : C)
    (g : ∀ j, f j ⟶ P) :
    sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j)

Proof state:
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
⊢ sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j)

Tactic:
ext j

Result:
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
j : β
⊢ Sigma.ι (fun b => G.obj (f b)) j ≫ sigmaComparison G f ≫ G.map (Sigma.desc g) =
    Sigma.ι (fun b => G.obj (f b)) j ≫ Sigma.desc fun j => G.map (g j)

Proof state:
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
j : β
⊢ Sigma.ι (fun b => G.obj (f b)) j ≫ sigmaComparison G f ≫ G.map (Sigma.desc g) =
    Sigma.ι (fun b => G.obj (f b)) j ≫ Sigma.desc fun j => G.map (g j)

Tactic:
simp only [Discrete.functor_obj, ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc,
  Cofan.mk_pt, Cofan.mk_ι_app]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.isUpperSet' {s : Finset α} (hs : (s : Set α).Intersecting)
    (h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t) : IsUpperSet (s : Set α)

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑(insert b s)

Tactic:
exact mem_insert_self _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ (↑(insert b s)).Intersecting

Tactic:
rw [coe_insert]

Result:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ (insert b ↑s).Intersecting

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑s

Tactic:
rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]

Result:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑(insert b s)

α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ (↑(insert b s)).Intersecting

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ IsUpperSet ↑s

Tactic:
rintro a b hab ha

Result:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑s

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ (insert b ↑s).Intersecting

Tactic:
exact
  hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1

Proof state:
x : ℂ
⊢ cos (2 * x) = 2 * cos x ^ 2 - 1

Tactic:
rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x), ← sub_add, sub_add_eq_add_sub,
  two_mul]

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem isEmpty_algebraRat_iff_mixedCharZero [CharZero R] :
    IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ∀ p > 0, ¬MixedCharZero R p

Tactic:
rw [not_isEmpty_iff, ← EqualCharZero.iff_not_mixedCharZero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ¬∃ p > 0, MixedCharZero R p

Tactic:
push_neg

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ∀ p > 0, ¬MixedCharZero R p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p

Tactic:
rw [← not_iff_not]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ¬∃ p > 0, MixedCharZero R p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
apply EqualCharZero.nonempty_algebraRat_iff

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem Quotient.subsingleton_iff {s : Setoid α} : Subsingleton (Quotient s) ↔ s = ⊤

Proof state:
α : Type u_1
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → s x y

Tactic:
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)

Result:
α : Type u_1
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → s a y

Proof state:
α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ ⊤ → s a b

Tactic:
simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']

Result:
no goals

Proof state:
α : Type u_1
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → s a y

Tactic:
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)

Result:
α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ ⊤ → s a b

Proof state:
α : Type u_1
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤

Tactic:
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply,
  forall_const]

Result:
α : Type u_1
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → s x y
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem eval₂_algebraMap_X {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (p : R[X])
    (f : R[X] →ₐ[R] A) : eval₂ (algebraMap R A) (f X) p = f p

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = ∑ x ∈ p.support, f (C (p.coeff x)) * f X ^ x

Tactic:
simp [Polynomial.C_eq_algebraMap]

Result:
no goals

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (f X) p = f (p.sum fun n a => C a * X ^ n)

Tactic:
simp only [eval₂_eq_sum, sum_def]

Result:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = f (∑ n ∈ p.support, C (p.coeff n) * X ^ n)

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = f (∑ n ∈ p.support, C (p.coeff n) * X ^ n)

Tactic:
simp only [map_sum, map_mul, map_pow, eq_intCast, map_intCast]

Result:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = ∑ x ∈ p.support, f (C (p.coeff x)) * f X ^ x

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (f X) p = f p

Tactic:
conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]

Result:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ eval₂ (algebraMap R A) (f X) p = f (p.sum fun n a => C a * X ^ n)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem abs_sinh (x : ℝ) : |sinh x| = sinh |x|

Proof state:
x : ℝ
⊢ |sinh x| = sinh |x|

Tactic:
cases le_total x 0 <;> simp [abs_of_nonneg, abs_of_nonpos, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_cons [Max α] [Std.Associative (max : α → α → α)] {xs : List α} :
    (x :: xs).max? = some (xs.max?.elim x (max x))

Proof state:
α : Type u_1
x : α
inst✝¹ : Max α
inst✝ : Std.Associative max
xs : List α
⊢ (x :: xs).max? = some (xs.max?.elim x (max x))

Tactic:
cases xs <;> simp [max?_cons', foldl_assoc]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem primeSpectrumProd_symm_inl_asIdeal (x : PrimeSpectrum R) :
    ((primeSpectrumProd R S).symm <| Sum.inl x).asIdeal = Ideal.prod x.asIdeal ⊤

Proof state:
case mk
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
asIdeal✝ : Ideal R
isPrime✝ : asIdeal✝.IsPrime
⊢ ((primeSpectrumProd R S).symm (Sum.inl { asIdeal := asIdeal✝, isPrime := isPrime✝ })).asIdeal =
    { asIdeal := asIdeal✝, isPrime := isPrime✝ }.asIdeal.prod ⊤

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
⊢ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod ⊤

Tactic:
cases x

Result:
case mk
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
asIdeal✝ : Ideal R
isPrime✝ : asIdeal✝.IsPrime
⊢ ((primeSpectrumProd R S).symm (Sum.inl { asIdeal := asIdeal✝, isPrime := isPrime✝ })).asIdeal =
    { asIdeal := asIdeal✝, isPrime := isPrime✝ }.asIdeal.prod ⊤
-- Mathlib/Data/Set/Function.lean
lemma graphOn_prod_graphOn (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
    s.graphOn f ×ˢ t.graphOn g = Equiv.prodProdProdComm .. ⁻¹' (s ×ˢ t).graphOn (Prod.map f g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn f s ×ˢ graphOn g t = ⇑(prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem two_pow_le_of_mem_bitIndices (ha : a ∈ n.bitIndices) : 2^a ≤ n

Proof state:
a n : ℕ
ha : a ∈ n.bitIndices
⊢ ∀ x ∈ map (fun i => 2 ^ i) n.bitIndices, 0 ≤ x

Tactic:
simp

Result:
no goals

Proof state:
a n : ℕ
ha : a ∈ n.bitIndices
⊢ 2 ^ a ≤ n

Tactic:
rw [← twoPowSum_bitIndices n]

Result:
a n : ℕ
ha : a ∈ n.bitIndices
⊢ 2 ^ a ≤ (map (fun i => 2 ^ i) n.bitIndices).sum

Proof state:
a n : ℕ
ha : a ∈ n.bitIndices
⊢ 2 ^ a ≤ (map (fun i => 2 ^ i) n.bitIndices).sum

Tactic:
exact List.single_le_sum (by simp) _ <| mem_map_of_mem _ ha

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem upperBound?_of_some {t : RBNode α} : ∃ x, t.upperBound? cut (some y) = some x

Proof state:
α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, upperBound? cut t (some y) = some x

Tactic:
induction t generalizing y <;> simp [upperBound?]

Result:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : ∀ {y : α}, ∃ x, upperBound? cut l✝ (some y) = some x
r_ih✝ : ∀ {y : α}, ∃ x, upperBound? cut r✝ (some y) = some x
y : α
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => upperBound? cut l✝ (some v✝)
      | Ordering.gt => upperBound? cut r✝ (some y)
      | Ordering.eq => some v✝) =
      some x

Proof state:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : ∀ {y : α}, ∃ x, upperBound? cut l✝ (some y) = some x
r_ih✝ : ∀ {y : α}, ∃ x, upperBound? cut r✝ (some y) = some x
y : α
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => upperBound? cut l✝ (some v✝)
      | Ordering.gt => upperBound? cut r✝ (some y)
      | Ordering.eq => some v✝) =
      some x

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean
theorem eisensteinSeries_SIF_MDifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
    MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (eisensteinSeries_SIF a k)

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ⇑(eisensteinSeries_SIF a k)

Tactic:
intro τ

Result:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (⇑(eisensteinSeries_SIF a k)) τ

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableAt ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ↑τ

Tactic:
refine DifferentiableOn.differentiableAt ?_
  ((isOpen_lt continuous_const Complex.continuous_im).mem_nhds τ.2)

Result:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableOn ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) {b | 0 < b.im}

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (⇑(eisensteinSeries_SIF a k)) τ

Tactic:
suffices DifferentiableAt ℂ (↑ₕeisensteinSeries_SIF a k) τ.1 by
  convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
  exact funext fun z ↦ (comp_ofComplex (eisensteinSeries_SIF a k) z).symm

Result:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableAt ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ↑τ

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ↑τ
⊢ MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (⇑(eisensteinSeries_SIF a k)) τ

Tactic:
convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe

Result:
case h.e'_21
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ↑τ
⊢ ⇑(eisensteinSeries_SIF a k) = (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ∘ Subtype.val

Proof state:
case h.e'_21
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ↑τ
⊢ ⇑(eisensteinSeries_SIF a k) = (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ∘ Subtype.val

Tactic:
exact funext fun z ↦ (comp_ofComplex (eisensteinSeries_SIF a k) z).symm

Result:
no goals

Proof state:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableOn ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) {b | 0 < b.im}

Tactic:
exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
  (Eventually.of_forall fun s ↦ DifferentiableOn.sum
    fun _ _ ↦ eisSummand_extension_differentiableOn _ _)
      (isOpen_lt continuous_const continuous_im)

Result:
no goals
-- Mathlib/Data/ENNReal/Holder.lean
lemma inv_sub_inv_eq_inv (hr : r ≠ 0) : r⁻¹ - q⁻¹ = p⁻¹

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr : r ≠ 0
⊢ q⁻¹ < ⊤

Tactic:
calc
  q⁻¹ ≤ r⁻¹ := HolderTriple.inv_le_inv q p r
  _ < ∞ := by simpa using pos_iff_ne_zero.mpr hr

Result:
no goals

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr : r ≠ 0
⊢ r⁻¹ < ⊤

Tactic:
simpa using pos_iff_ne_zero.mpr hr

Result:
no goals

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr : r ≠ 0
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
apply ENNReal.sub_eq_of_eq_add (ne_of_lt ?_) (inv_eq p q r)

Result:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr : r ≠ 0
⊢ q⁻¹ < ⊤
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_nodal_at_node {i : ι} (hi : i ∈ s) : eval (v i) (nodal s v) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ eval (v i) (nodal s v) = 0

Tactic:
rw [eval_nodal]

Result:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ ∏ i_1 ∈ s, (v i - v i_1) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ ∏ i_1 ∈ s, (v i - v i_1) = 0

Tactic:
exact s.prod_eq_zero hi (sub_self (v i))

Result:
no goals