harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_intCast_num (a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a

Proof state:
case inr.inl

⊢ (↑0)⁻¹.num = Int.sign 0

Tactic:
simp

Result:
no goals

Proof state:
case inl.intro
a : ℤ
lt : 0 < a
⊢ (↑(-a))⁻¹.num = (-a).sign

Tactic:
simp [Rat.inv_neg, inv_intCast_num_of_pos lt, Int.sign_eq_one_iff_pos.mpr lt]

Result:
no goals

Proof state:
case inr.inr
a : ℤ
gt : 0 < a
⊢ (↑a)⁻¹.num = a.sign

Tactic:
simp [inv_intCast_num_of_pos gt, Int.sign_eq_one_iff_pos.mpr gt]

Result:
no goals

Proof state:
case inl
a : ℤ
lt : a < 0
⊢ (↑a)⁻¹.num = a.sign

Tactic:
obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩

Result:
case inl.intro
a : ℤ
lt : -a < 0
⊢ (↑(-a))⁻¹.num = (-a).sign

Proof state:
a : ℤ
⊢ (↑a)⁻¹.num = a.sign

Tactic:
rcases lt_trichotomy a 0 with lt | rfl | gt

Result:
case inl
a : ℤ
lt : a < 0
⊢ (↑a)⁻¹.num = a.sign

case inr.inl

⊢ (↑0)⁻¹.num = Int.sign 0

case inr.inr
a : ℤ
gt : 0 < a
⊢ (↑a)⁻¹.num = a.sign

Proof state:
case inl.intro
a : ℤ
lt : -a < 0
⊢ (↑(-a))⁻¹.num = (-a).sign

Tactic:
simp at lt

Result:
case inl.intro
a : ℤ
lt : 0 < a
⊢ (↑(-a))⁻¹.num = (-a).sign
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih1_neg_left : IH1 x y → IH1 (-x) y :=
  fun h x₁ x₂ y' h₁ h₂ hy ↦ by
    rw [isOption_neg] at h₁ h₂
    exact P24_neg_left.2 (h h₂ h₁ hy)

Proof state:
x y : PGame
h : IH1 x y
x₁ x₂ y' : PGame
h₁ : (-x₁).IsOption x
h₂ : (-x₂).IsOption x
hy : y' = y ∨ y'.IsOption y
⊢ P24 x₁ x₂ y'

Tactic:
exact P24_neg_left.2 (h h₂ h₁ hy)

Result:
no goals

Proof state:
x y : PGame
h : IH1 x y
x₁ x₂ y' : PGame
h₁ : x₁.IsOption (-x)
h₂ : x₂.IsOption (-x)
hy : y' = y ∨ y'.IsOption y
⊢ P24 x₁ x₂ y'

Tactic:
rw [isOption_neg] at h₁ h₂

Result:
x y : PGame
h : IH1 x y
x₁ x₂ y' : PGame
h₁ : (-x₁).IsOption x
h₂ : (-x₂).IsOption x
hy : y' = y ∨ y'.IsOption y
⊢ P24 x₁ x₂ y'
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_neg_of_pos_of_neg [PosSMulStrictMono α β] (ha : 0 < a) (hb : b < 0) : a • b < 0

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulStrictMono α β
ha : 0 < a
hb : b < 0
⊢ a • b < 0

Tactic:
simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem size_clearUnit_foldl {α : Type u} (assignments : Array Assignment)
    (f : Array Assignment → α → Array Assignment) (f_preserves_size :
    ∀ arr : Array Assignment, ∀ a : α, (f arr a).size = arr.size) (l : List α) :
  Array.size (List.foldl f assignments l) = Array.size assignments

Proof state:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
assignments' : Array Assignment
hsize : assignments'.size = assignments.size
a : α
x✝ : a ∈ l
⊢ (f assignments' a).size = assignments.size

Tactic:
rw [f_preserves_size assignments' a, hsize]

Result:
no goals

Proof state:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
⊢ (List.foldl f assignments l).size = assignments.size

Tactic:
have hb : assignments.size = assignments.size := rfl

Result:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size

Proof state:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size

Tactic:
have hl (assignments' : Array Assignment) (hsize : assignments'.size = assignments.size) (a : α) (_ : a ∈ l) :
  (f assignments' a).size = assignments.size := by rw [f_preserves_size assignments' a, hsize]

Result:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
hl :
  ∀ (assignments' : Array Assignment),
    assignments'.size = assignments.size → ∀ (a : α), a ∈ l → (f assignments' a).size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size

Proof state:
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
hl :
  ∀ (assignments' : Array Assignment),
    assignments'.size = assignments.size → ∀ (a : α), a ∈ l → (f assignments' a).size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size

Tactic:
exact List.foldlRecOn l f assignments hb hl

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem support_add_single {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
    support (f + single a b) = cons a f.support ha

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (f + single a b).support = cons a f.support ha

Tactic:
rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]

Result:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (f + single a b).support = cons a f.support ha

Tactic:
have H := support_single_ne_zero a hb

Result:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ (f + single a b).support = cons a f.support ha

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support

Tactic:
rwa [H, disjoint_singleton_right]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
b : M
f : α →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (f + single a b).support = cons a f.support ha

Tactic:
classical
have H := support_single_ne_zero a hb
rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
rwa [H, disjoint_singleton_right]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_singleton {b : β} : s ×ˢ {b} = s.map ⟨fun i => (i, b), Prod.mk.inj_right _⟩

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
b : β
⊢ s ×ˢ {b} = map { toFun := fun i => (i, b), inj' := ⋯ } s

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ map { toFun := fun i => (i, b), inj' := ⋯ } s

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ map { toFun := fun i => (i, b), inj' := ⋯ } s

Tactic:
simp [and_left_comm, eq_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.finrank_pi_fintype
    {ι : Type v} [Fintype ι] {M : ι → Type w} [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] :
    finrank R (∀ i, M i) = ∑ i, finrank R (M i)

Proof state:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)

Tactic:
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma,
  mk_toNat_eq_card, Fintype.card_sigma]

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)

Tactic:
letI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem cons_subset : a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m

Proof state:
α✝ : Type u_1
a : α✝
l m : List α✝
⊢ a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m

Tactic:
simp only [subset_def, mem_cons, or_imp, forall_and, forall_eq]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem getLastI_eq_getLast? [Inhabited α] : ∀ l : List α, l.getLastI = l.getLast?.iget
  | [] => by simp [getLastI, Inhabited.default]
  | [_] => rfl
  | [_, _] => rfl
  | [_, _, _] => rfl
  | _ :: _ :: c :: l => by simp [getLastI, getLastI_eq_getLast? (c :: l)]

Proof state:
α : Type u
inst✝ : Inhabited α
head✝¹ head✝ c : α
l : List α
⊢ (head✝¹ :: head✝ :: c :: l).getLastI = (head✝¹ :: head✝ :: c :: l).getLast?.iget

Tactic:
simp [getLastI, getLastI_eq_getLast? (c :: l)]

Result:
no goals

Proof state:
α : Type u
inst✝ : Inhabited α
⊢ [].getLastI = [].getLast?.iget

Tactic:
simp [getLastI, Inhabited.default]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem hasProd_lt (h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁) (hg : HasProd g a₂) :
    a₁ < a₂

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁
hg : HasProd g a₂
this : update f i 1 ≤ update g i 1
⊢ a₁ < a₂

Tactic:
have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)

Result:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁
hg : HasProd g a₂
this✝ : update f i 1 ≤ update g i 1
this : 1 / f i * a₁ ≤ 1 / g i * a₂
⊢ a₁ < a₂

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁
hg : HasProd g a₂
⊢ a₁ < a₂

Tactic:
have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩

Result:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁
hg : HasProd g a₂
this : update f i 1 ≤ update g i 1
⊢ a₁ < a₂

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁
hg : HasProd g a₂
this✝ : update f i 1 ≤ update g i 1
this : 1 / f i * a₁ ≤ 1 / g i * a₂
⊢ a₁ < a₂

Tactic:
simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁
hg : HasProd g a₂
⊢ a₁ < a₂

Tactic:
classical
have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem idxOf_cons_eq {a b : α} (l : List α) : b = a → idxOf a (b :: l) = 0
  | e => by rw [← e]; exact idxOf_cons_self

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0

Tactic:
exact idxOf_cons_self

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf a (b :: l) = 0

Tactic:
rw [← e]

Result:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0
-- Mathlib/Data/Holor.lean
theorem cast_type (eq : ds₁ = ds₂) (a : Holor α ds₁) :
    cast (congr_arg (Holor α) eq) a = fun t => a (cast (congr_arg HolorIndex eq.symm) t)

Proof state:
α : Type
ds₁ ds₂ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
⊢ cast ⋯ a = fun t => a (cast ⋯ t)

Tactic:
subst eq

Result:
α : Type
ds₁ : List ℕ
a : Holor α ds₁
⊢ cast ⋯ a = fun t => a (cast ⋯ t)

Proof state:
α : Type
ds₁ : List ℕ
a : Holor α ds₁
⊢ cast ⋯ a = fun t => a (cast ⋯ t)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_injective2 : Function.Injective2 (@snoc n α) := fun x y xₙ yₙ h ↦
  ⟨funext fun i ↦ by simpa using congr_fun h (castSucc i), by simpa using congr_fun h (last n)⟩

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
⊢ xₙ = yₙ

Tactic:
simpa using congr_fun h (last n)

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (castSucc i)

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem isNilpotent_toEnd_genWeightSpace_zero [IsNoetherian R M] (x : L) :
    _root_.IsNilpotent <| toEnd R L (genWeightSpace M (0 : L → R)) x

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
x : L
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M 0)) x)

Tactic:
simpa using isNilpotent_toEnd_sub_algebraMap M (0 : L → R) x

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma cauchy_iff_le {l : Filter α} [hl : l.NeBot] :
    Cauchy l ↔ l ×ˢ l ≤ 𝓤 α

Proof state:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
hl : l.NeBot
⊢ Cauchy l ↔ l ×ˢ l ≤ 𝓤 α

Tactic:
simp only [Cauchy, hl, true_and]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem dFrom_eq {i j : ι} (r : c.Rel i j) : C.dFrom i = C.d i j ≫ (C.xNextIso r).inv

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i = C.d i j ≫ (C.xNextIso r).inv

Tactic:
obtain rfl := c.next_eq' r

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
r : c.Rel i (c.next i)
⊢ C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
r : c.Rel i (c.next i)
⊢ C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv

Tactic:
exact (Category.comp_id _).symm

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_natCast (n : ℕ) : ⌊(n : α)⌋₊ = n :=
  eq_of_forall_le_iff fun a => by
    rw [le_floor_iff, Nat.cast_le]
    exact n.cast_nonneg

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
n a : ℕ
⊢ a ≤ ⌊↑n⌋₊ ↔ a ≤ n

Tactic:
rw [le_floor_iff, Nat.cast_le]

Result:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
n a : ℕ
⊢ 0 ≤ ↑n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
n a : ℕ
⊢ 0 ≤ ↑n

Tactic:
exact n.cast_nonneg

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_ge_nat {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * n) n, c * f n ≤ f u

Proof state:
case intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u

Tactic:
exact ⟨c, hc_mem, hc.natCast_atTop⟩

Result:
no goals

Proof state:
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u

Tactic:
obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_ge hb

Result:
case intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_ne_zero_iff (x y : E) : o.kahler x y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ x = 0 ∨ y = 0 → ↑(inner x y) + ↑((o.areaForm x) y) * Complex.I = 0

Tactic:
rintro (rfl | rfl) <;> simp

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) y ≠ 0 → x ≠ 0 ∧ y ≠ 0

Tactic:
contrapose

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ¬(x ≠ 0 ∧ y ≠ 0) → ¬(o.kahler x) y ≠ 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ¬(x ≠ 0 ∧ y ≠ 0) → ¬(o.kahler x) y ≠ 0

Tactic:
simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ x = 0 ∨ y = 0 → ↑(inner x y) + ↑((o.areaForm x) y) * Complex.I = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0

Tactic:
refine ⟨?_, fun h => o.kahler_ne_zero h.1 h.2⟩

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) y ≠ 0 → x ≠ 0 ∧ y ≠ 0
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem sum_four_squares (n : ℕ) : ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

Proof state:
case h.intro.intro.intro.intro.intro.intro.intro.intro
a b c d w x y z : ℕ
⊢ ∃ a_1 b_1 c_1 d_1,
    a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2)

Tactic:
exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩

Result:
no goals

Proof state:
case h0

⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 0

Tactic:
exact ⟨0, 0, 0, 0, rfl⟩

Result:
no goals

Proof state:
case h
m n : ℕ
hm : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * n

Tactic:
rcases hm with ⟨a, b, c, d, rfl⟩

Result:
case h.intro.intro.intro.intro
n : ℕ
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
a b c d : ℕ
⊢ ∃ a_1 b_1 c_1 d_1, a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * n

Proof state:
case hp
p : ℕ
hp : Prime p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
exact hp.sum_four_squares

Result:
no goals

Proof state:
n : ℕ
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

Tactic:
induction n using Nat.recOnMul with
| h0 => exact ⟨0, 0, 0, 0, rfl⟩
| h1 => exact ⟨1, 0, 0, 0, rfl⟩
| hp p hp => exact hp.sum_four_squares
| h m n hm hn =>
  rcases hm with ⟨a, b, c, d, rfl⟩
  rcases hn with ⟨w, x, y, z, rfl⟩
  exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩

Result:
no goals

Proof state:
case h1

⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1

Tactic:
exact ⟨1, 0, 0, 0, rfl⟩

Result:
no goals

Proof state:
case h.intro.intro.intro.intro
n : ℕ
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
a b c d : ℕ
⊢ ∃ a_1 b_1 c_1 d_1, a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * n

Tactic:
rcases hn with ⟨w, x, y, z, rfl⟩

Result:
case h.intro.intro.intro.intro.intro.intro.intro.intro
a b c d w x y z : ℕ
⊢ ∃ a_1 b_1 c_1 d_1,
    a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2)
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem map_smul₂ (f : E →L[𝕜] F →L[𝕜] G) (c : 𝕜) (x : E) (y : F) : f (c • x) y = c • f x y

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
c : 𝕜
x : E
y : F
⊢ (f (c • x)) y = c • (f x) y

Tactic:
rw [f.map_smul, smul_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem le_mul_iff_one_le_right' [MulLeftMono α]
    [MulLeftReflectLE α] (a : α) {b : α} :
    a ≤ a * b ↔ 1 ≤ b :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_iff_left a)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
a b : α
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_singleton (a : α) (p : α → Bool) :
    #[a].find? p = if p a then some a else none

Proof state:
α : Type u_1
a : α
p : α → Bool
⊢ find? p #[a] = if p a = true then some a else none

Tactic:
simp [singleton_eq_toArray_singleton]

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem nodup_add {s t : Multiset α} : Nodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t :=
  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append]

Proof state:
α : Type u_1
s t : Multiset α
x✝¹ x✝ : List α
⊢ (⟦x✝¹⟧ + ⟦x✝⟧).Nodup ↔ Nodup ⟦x✝¹⟧ ∧ Nodup ⟦x✝⟧ ∧ _root_.Disjoint ⟦x✝¹⟧ ⟦x✝⟧

Tactic:
simp [nodup_append]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_neg (f : N →ₗ[R] P) : (-f).rTensor M = -f.rTensor M

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ (rTensorHom M) (-f) = -(rTensorHom M) f

Tactic:
exact (rTensorHom (R := R) (N := N) (P := P) M).map_neg f

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ rTensor M (-f) = -rTensor M f

Tactic:
simp only [← coe_rTensorHom]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ (rTensorHom M) (-f) = -(rTensorHom M) f