harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_lt {x : α} [LinearOrderedSemifield α] [CanonicallyOrderedAdd α]
    [Sub α] [OrderedSub α]
    (h0 : x ≠ 0) (h1 : x < 1) (n : ℕ) : ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Proof state:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 ∧ 0 < x ^ n

Tactic:
exact ⟨h0.trans h1, pow_pos h0 n⟩

Result:
no goals

Proof state:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ≠ 0

Tactic:
rwa [ne_eq, tsub_eq_zero_iff_le, not_le]

Result:
no goals

Proof state:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x

Tactic:
rwa [tsub_pos_iff_lt]

Result:
no goals

Proof state:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : x ≠ 0
h1 : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Tactic:
rw [← pos_iff_ne_zero] at h0

Result:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Proof state:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Tactic:
rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]

Result:
α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 ∧ 0 < x ^ n

α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ≠ 0

α : Type u
x : α
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
theorem map_add {F} [Add β] [FunLike F α β] [AddHomClass F α β]
    (f : F) (a b : WithBot α) :
    (a + b).map f = a.map f + b.map f

Proof state:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ⇑f ↑(a✝¹ + a✝) = ↑(f (a✝¹ + a✝))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithBot α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
induction a

Result:
case bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
⊢ map (⇑f) (⊥ + b) = map ⇑f ⊥ + map (⇑f) b

case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Proof state:
case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
induction b

Result:
case coe.bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊥) = map ⇑f ↑a✝ + map ⇑f ⊥

case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Proof state:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]

Result:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ⇑f ↑(a✝¹ + a✝) = ↑(f (a✝¹ + a✝))

Proof state:
case bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
⊢ map (⇑f) (⊥ + b) = map ⇑f ⊥ + map (⇑f) b

Tactic:
exact (bot_add _).symm

Result:
no goals

Proof state:
case coe.bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊥) = map ⇑f ↑a✝ + map ⇑f ⊥

Tactic:
exact (add_bot _).symm

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_φ (n : ℤ) : (W.baseChange B).φ n = ((W.baseChange A).φ n).map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W.baseChange B).φ n = Polynomial.map (mapRingHom ↑f) ((W.baseChange A).φ n)

Tactic:
rw [← map_φ, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_modifyKey_self [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) : getValue? k (modifyKey k f l) = (getValue? k l).map f

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValue? k (modifyKey k f l) = Option.map f (getValue? k l)

Tactic:
simp [getValue?_modifyKey, hl]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem IsUpperSet.not_bddAbove (hs : IsUpperSet s) : s.Nonempty → ¬BddAbove s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False

Tactic:
exact hc.not_le (hb <| hs ((hb ha).trans hc.le) ha)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
⊢ s.Nonempty → ¬BddAbove s

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_gt b

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem _root_.Multiset.prod_X_sub_C_dvd_iff_le_roots {p : R[X]} (hp : p ≠ 0) (s : Multiset R) :
    (s.map fun a => X - C a).prod ∣ p ↔ s ≤ p.roots

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
⊢ (Multiset.map (fun a => X - C a) s).prod ∣ p ↔ s ≤ p.roots

Tactic:
exact
⟨fun h =>
Multiset.le_iff_count.2 fun r => by
rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
fun h =>
(Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a => X - C a) s).prod ∣ p
r : R
⊢ count r s ≤ count r p.roots

Tactic:
rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
  Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a => X - C a) s).prod ∣ p
r : R
⊢ (Multiset.map (fun a => X - C a) (Multiset.filter (Eq r) s)).prod ∣ p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a => X - C a) s).prod ∣ p
r : R
⊢ (Multiset.map (fun a => X - C a) (Multiset.filter (Eq r) s)).prod ∣ p

Tactic:
exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
⊢ (Multiset.map (fun a => X - C a) s).prod ∣ p ↔ s ≤ p.roots

Tactic:
classical exact
⟨fun h =>
  Multiset.le_iff_count.2 fun r => by
    rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
      Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
    exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
  fun h =>
  (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
/-- We show that the partial order and the topology on `ℂ` are compatible.
We turn this into an instance scoped to `ComplexOrder`. -/
lemma orderClosedTopology : OrderClosedTopology ℂ where
  isClosed_le'

Proof state:
⊢ IsClosed {p | p.1 ≤ p.2}

Tactic:
simp_rw [le_def, Set.setOf_and]

Result:
⊢ IsClosed ({a | a.1.re ≤ a.2.re} ∩ {a | a.1.im = a.2.im})

Proof state:
⊢ IsClosed ({a | a.1.re ≤ a.2.re} ∩ {a | a.1.im = a.2.im})

Tactic:
refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> continuity

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
theorem exists_norm_finset_prod_le (t : Finset ι) [Nonempty ι] (f : ι → M) :
    ∃ i : ι, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Proof state:
case inr
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
t : Finset ι
inst✝ : Nonempty ι
f : ι → M
ht : t.Nonempty
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Tactic:
exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <| exists_norm_finset_prod_le_of_nonempty ht f

Result:
no goals

Proof state:
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
t : Finset ι
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Result:
case inl
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (∅.Nonempty → i ∈ ∅) ∧ ‖∏ j ∈ ∅, f j‖ ≤ ‖f i‖

case inr
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
t : Finset ι
inst✝ : Nonempty ι
f : ι → M
ht : t.Nonempty
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Proof state:
case inl
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (∅.Nonempty → i ∈ ∅) ∧ ‖∏ j ∈ ∅, f j‖ ≤ ‖f i‖

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb_and {x : BitVec w} {hi lo : Nat} :
   (x &&& y).extractLsb lo hi = (x.extractLsb lo hi) &&& (y.extractLsb lo hi)

Proof state:
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ k ≤ lo - hi

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ (extractLsb lo hi (x &&& y)).getLsbD k = (extractLsb lo hi x &&& extractLsb lo hi y).getLsbD k

Tactic:
simp [hk, show k ≤ lo - hi by omega]

Result:
no goals

Proof state:
w : Nat
y x : BitVec w
hi lo : Nat
⊢ extractLsb lo hi (x &&& y) = extractLsb lo hi x &&& extractLsb lo hi y

Tactic:
ext k hk

Result:
case pred
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ (extractLsb lo hi (x &&& y)).getLsbD k = (extractLsb lo hi x &&& extractLsb lo hi y).getLsbD k
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem list_prod_subset_list_prod (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) :
    (t.map f₁).prod ⊆ (t.map f₂).prod

Proof state:
case nil
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
hf : ∀ i ∈ [], f₁ i ⊆ f₂ i
⊢ (List.map f₁ []).prod ⊆ (List.map f₂ []).prod

Tactic:
rfl

Result:
no goals

Proof state:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ (List.map f₁ (h :: tl)).prod ⊆ (List.map f₂ (h :: tl)).prod

Tactic:
simp_rw [List.map_cons, List.prod_cons]

Result:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ f₁ h * (List.map f₁ tl).prod ⊆ f₂ h * (List.map f₂ tl).prod

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (List.map f₁ t).prod ⊆ (List.map f₂ t).prod

Tactic:
induction' t with h tl ih

Result:
case nil
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
hf : ∀ i ∈ [], f₁ i ⊆ f₂ i
⊢ (List.map f₁ []).prod ⊆ (List.map f₂ []).prod

case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ (List.map f₁ (h :: tl)).prod ⊆ (List.map f₂ (h :: tl)).prod

Proof state:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ f₁ h * (List.map f₁ tl).prod ⊆ f₂ h * (List.map f₂ tl).prod

Tactic:
exact mul_subset_mul (hf h <| List.mem_cons_self _ _)
  (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem strictConvexOn_pow {n : ℕ} (hn : 2 ≤ n) : StrictConvexOn ℝ (Ici 0) fun x : ℝ => x ^ n

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (fun x => ↑n * x ^ (n - 1)) (Ioi 0)

Tactic:
exact fun x (hx : 0 < x) y _ hxy => mul_lt_mul_of_pos_left
  (pow_lt_pow_left₀ hxy hx.le <| Nat.sub_ne_zero_of_lt hn) (by positivity)

Result:
no goals

Proof state:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 0 < x
y : ℝ
x✝ : y ∈ Ioi 0
hxy : x < y
⊢ 0 < ↑n

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ StrictConvexOn ℝ (Ici 0) fun x => x ^ n

Tactic:
apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _)

Result:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (deriv fun x => x ^ n) (interior (Ici 0))

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (deriv fun x => x ^ n) (interior (Ici 0))

Tactic:
rw [deriv_pow', interior_Ici]

Result:
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (fun x => ↑n * x ^ (n - 1)) (Ioi 0)
-- Mathlib/ModelTheory/Quotients.lean
theorem Term.realize_quotient_mk' {β : Type*} (t : L.Term β) (x : β → M) :
    (t.realize fun i => (⟦x i⟧ : Quotient s)) = ⟦@Term.realize _ _ ps.toStructure _ x t⟧

Proof state:
case var
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
a✝ : β
⊢ realize (fun i => ⟦x i⟧) (var a✝) = ⟦realize x (var a✝)⟧

Tactic:
rfl

Result:
no goals

Proof state:
case func
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
ih : ∀ (a : Fin l✝), realize (fun i => ⟦x i⟧) (_ts✝ a) = ⟦realize x (_ts✝ a)⟧
⊢ realize (fun i => ⟦x i⟧) (func _f✝ _ts✝) = ⟦realize x (func _f✝ _ts✝)⟧

Tactic:
simp only [ih, funMap_quotient_mk', Term.realize]

Result:
no goals

Proof state:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
t : L.Term β
x : β → M
⊢ realize (fun i => ⟦x i⟧) t = ⟦realize x t⟧

Tactic:
induction t with
| var => rfl
| func _ _ ih => simp only [ih, funMap_quotient_mk', Term.realize]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem two_le_card_support_cycleOf_iff [DecidableEq α] [Fintype α] :
    2 ≤ #(cycleOf f x).support ↔ f x ≠ x

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ 2 ≤ #(f.cycleOf x).support ↔ f x ≠ x

Tactic:
refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩

Result:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : 2 ≤ #(f.cycleOf x).support
⊢ f x ≠ x

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x ≠ x
⊢ 2 ≤ #(f.cycleOf x).support

Tactic:
simpa using (isCycle_cycleOf _ h).two_le_card_support

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x = x
⊢ #(f.cycleOf x).support < 2

Tactic:
rw [← cycleOf_eq_one_iff] at h

Result:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : 2 ≤ #(f.cycleOf x).support
⊢ f x ≠ x

Tactic:
contrapose! h

Result:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x = x
⊢ #(f.cycleOf x).support < 2
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem length_eq {l : AssocList α β} : l.length = l.toList.length

Proof state:
α : Type u
β : α → Type v
l : AssocList α β
⊢ ∀ (n : Nat), List.foldl (fun d x => d + 1) n l.toList = l.toList.length + n

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
⊢ ∀ (n : Nat), List.foldl (fun d x => d + 1) n nil.toList = nil.toList.length + n

case cons
α : Type u
β : α → Type v
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : ∀ (n : Nat), List.foldl (fun d x => d + 1) n tail✝.toList = tail✝.toList.length + n
⊢ ∀ (n : Nat),
    List.foldl (fun d x => d + 1) n (cons key✝ value✝ tail✝).toList = (cons key✝ value✝ tail✝).toList.length + n

Proof state:
case cons
α : Type u
β : α → Type v
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : ∀ (n : Nat), List.foldl (fun d x => d + 1) n tail✝.toList = tail✝.toList.length + n
⊢ ∀ (n : Nat),
    List.foldl (fun d x => d + 1) n (cons key✝ value✝ tail✝).toList = (cons key✝ value✝ tail✝).toList.length + n

Tactic:
next _ _ t ih =>
intro n
simp [ih, Nat.add_assoc, Nat.add_comm n 1]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
l : AssocList α β
⊢ List.foldl (fun d p => d + 1) 0 l.toList = l.toList.length

Tactic:
suffices ∀ n, l.toList.foldl (fun d _ => d + 1) n = l.toList.length + n by simp

Result:
α : Type u
β : α → Type v
l : AssocList α β
⊢ ∀ (n : Nat), List.foldl (fun d x => d + 1) n l.toList = l.toList.length + n

Proof state:
α : Type u
β : α → Type v
l : AssocList α β
this : ∀ (n : Nat), List.foldl (fun d x => d + 1) n l.toList = l.toList.length + n
⊢ List.foldl (fun d p => d + 1) 0 l.toList = l.toList.length

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
⊢ ∀ (n : Nat), List.foldl (fun d x => d + 1) n nil.toList = nil.toList.length + n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
l : AssocList α β
⊢ l.length = l.toList.length

Tactic:
rw [length, foldl_eq]

Result:
α : Type u
β : α → Type v
l : AssocList α β
⊢ List.foldl (fun d p => d + 1) 0 l.toList = l.toList.length

Proof state:
α : Type u
β : α → Type v
key✝ : α
value✝ : β key✝
t : AssocList α β
ih : ∀ (n : Nat), List.foldl (fun d x => d + 1) n t.toList = t.toList.length + n
n : Nat
⊢ List.foldl (fun d x => d + 1) n (cons key✝ value✝ t).toList = (cons key✝ value✝ t).toList.length + n

Tactic:
simp [ih, Nat.add_assoc, Nat.add_comm n 1]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
key✝ : α
value✝ : β key✝
t : AssocList α β
ih : ∀ (n : Nat), List.foldl (fun d x => d + 1) n t.toList = t.toList.length + n
⊢ ∀ (n : Nat), List.foldl (fun d x => d + 1) n (cons key✝ value✝ t).toList = (cons key✝ value✝ t).toList.length + n

Tactic:
intro n

Result:
α : Type u
β : α → Type v
key✝ : α
value✝ : β key✝
t : AssocList α β
ih : ∀ (n : Nat), List.foldl (fun d x => d + 1) n t.toList = t.toList.length + n
n : Nat
⊢ List.foldl (fun d x => d + 1) n (cons key✝ value✝ t).toList = (cons key✝ value✝ t).toList.length + n
-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma commShiftIso_comp_hom_app [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
    (commShiftIso (F ⋙ G) a).hom.app X =
      G.map ((commShiftIso F a).hom.app X) ≫ (commShiftIso G a).hom.app (F.obj X)

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_7, u_2} D
inst✝⁶ : Category.{u_8, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a : A
X : C
⊢ ((F ⋙ G).commShiftIso a).hom.app X = G.map ((F.commShiftIso a).hom.app X) ≫ (G.commShiftIso a).hom.app (F.obj X)

Tactic:
simp [commShiftIso, CommShift.iso]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem fp_iff_derivBFamily (H : ∀ i hi, IsNormal (f i hi)) {a} :
    (∀ i hi, f i hi a = a) ↔ ∃ b, derivBFamily.{u, v} o f b = a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∃ b, o.derivBFamily f b = a

Tactic:
rw [← le_iff_derivBFamily H]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a

Tactic:
refine ⟨fun h i hi => le_of_eq (h i hi), fun h i hi => ?_⟩

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a = a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a ≤ a

Tactic:
exact h i hi

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a = a

Tactic:
rw [← (H i hi).le_iff_eq]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a ≤ a
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_addX (P Q : Fin 3 → A) : (W'.baseChange B).toProjective.addX (f ∘ P) (f ∘ Q) =
    f ((W'.baseChange A).toProjective.addX P Q)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toProjective.addX (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toProjective.addX P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

Result:
no goals