harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Max.lean
theorem min_eq_top {s : Finset α} : s.min = ⊤ ↔ s = ∅

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ s.min = ⊤ ↔ s = ∅

Tactic:
simp [Finset.min, eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
lemma epi_f [IsFiltered J] : Epi (f z)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ Epi (f z)

Tactic:
have := isIso_f hc z

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
this : IsIso (f z)
⊢ Epi (f z)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
this : IsIso (f z)
⊢ Epi (f z)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_zero : preNormEDS b c d 0 = 0

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 0 = 0

Tactic:
erw [preNormEDS_ofNat, preNormEDS'_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ Action V G` preserves the limit of some `K : J ⥤ C` if
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
lemma preservesLimit_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
    [Category.{w₂} J] (K : J ⥤ C)
    (h : PreservesLimit K (F ⋙ Action.forget V G)) : PreservesLimit K F

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
this : PreservesLimit K F'
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

Result:
no goals

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
⊢ PreservesLimit K F

Tactic:
let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor

Result:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
⊢ PreservesLimit K F

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
⊢ PreservesLimit K F

Tactic:
have : PreservesLimit K F' := SingleObj.preservesLimit _ _ h

Result:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
this : PreservesLimit K F'
⊢ PreservesLimit K F
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma pow_dvd_sub_pow_of_pow_eq_zero_right (hp : n + m ≤ p + 1) (h_comm : Commute x y)
    (hy : y ^ n = 0) : x ^ m ∣ (x - y) ^ p :=
  (sub_right rfl h_comm).pow_dvd_pow_of_sub_pow_eq_zero hp (by simpa)

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ (x - (x - y)) ^ n = 0

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_append (xs ys : Array α) :
    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩

Proof state:
α : Type u_1
xs ys : Array α
⊢ (xs ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        ys.attach

Tactic:
cases xs

Result:
case mk
α : Type u_1
ys : Array α
toList✝ : List α
⊢ ({ toList := toList✝ } ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        ys.attach

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (toList✝¹ ++ toList✝).toArray.attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝¹ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝ }.attach

Tactic:
simp [List.attach_append, Function.comp_def]

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝¹ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝ }.attach

Tactic:
rw [attach_congr (List.append_toArray _ _)]

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (toList✝¹ ++ toList✝).toArray.attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝¹ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝ }.attach

Proof state:
case mk
α : Type u_1
ys : Array α
toList✝ : List α
⊢ ({ toList := toList✝ } ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        ys.attach

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝¹ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toList := toList✝ }.attach
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_max_aux₃ {f : ℂ → F} {z w : ℂ} {r : ℝ} (hr : dist w z = r)
    (hd : DiffContOnCl ℂ f (ball z r)) (hz : IsMaxOn (norm ∘ f) (ball z r) z) : ‖f w‖ = ‖f z‖

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
rcases eq_or_ne w z with (rfl | hne)

Result:
case inl
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
w : ℂ
hd : DiffContOnCl ℂ f (ball w (dist w w))
hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w
⊢ ‖f w‖ = ‖f w‖

case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖

Proof state:
case inl
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
w : ℂ
hd : DiffContOnCl ℂ f (ball w (dist w w))
hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w
⊢ ‖f w‖ = ‖f w‖

Tactic:
rfl

Result:
no goals

Proof state:
case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : dist w z ≠ 0
⊢ ‖f w‖ = ‖f z‖

Tactic:
exact norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuousOn.norm)

Result:
no goals

Proof state:
case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖

Tactic:
rw [← dist_ne_zero] at hne

Result:
case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : dist w z ≠ 0
⊢ ‖f w‖ = ‖f z‖

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
subst r

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_mul (s : Set ι) (f g : ι → M₀) :
    indicator s (fun i ↦ f i * g i) = fun i ↦ indicator s f i * indicator s g i

Proof state:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

Tactic:
rfl

Result:
no goals

Proof state:
case h
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 0) = (if x✝ ∈ s then f x✝ else 0) * if x✝ ∈ s then g x✝ else 0

Tactic:
split_ifs

Result:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : x✝ ∉ s
⊢ 0 = 0 * 0

Proof state:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : x✝ ∉ s
⊢ 0 = 0 * 0

Tactic:
rw [mul_zero]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
⊢ (s.indicator fun i => f i * g i) = fun i => s.indicator f i * s.indicator g i

Tactic:
funext

Result:
case h
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
⊢ s.indicator (fun i => f i * g i) x✝ = s.indicator f x✝ * s.indicator g x✝

Proof state:
case h
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
⊢ s.indicator (fun i => f i * g i) x✝ = s.indicator f x✝ * s.indicator g x✝

Tactic:
simp only [indicator]

Result:
case h
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 0) = (if x✝ ∈ s then f x✝ else 0) * if x✝ ∈ s then g x✝ else 0
-- Mathlib/Order/LiminfLimsup.lean
lemma IsBoundedUnder.eventually_le (h : IsBoundedUnder (· ≤ ·) f u) :
    ∃ a, ∀ᶠ x in f, u x ≤ a

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
a : α
ha : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x a
⊢ ∀ᶠ (x : β) in f, u x ≤ a

Tactic:
exact eventually_map.1 ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
⊢ ∃ a, ∀ᶠ (x : β) in f, u x ≤ a

Tactic:
obtain ⟨a, ha⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
a : α
ha : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x a
⊢ ∃ a, ∀ᶠ (x : β) in f, u x ≤ a

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
a : α
ha : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x a
⊢ ∃ a, ∀ᶠ (x : β) in f, u x ≤ a

Tactic:
use a

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
a : α
ha : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x a
⊢ ∀ᶠ (x : β) in f, u x ≤ a
-- Mathlib/Topology/Order/Compact.lean
theorem IsCompact.bddBelow [ClosedIicTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) :
    BddBelow s

Proof state:
case inr.intro.intro
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
a : α
has : a ∈ lowerBounds s
⊢ BddBelow s

Tactic:
exact ⟨a, has⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
⊢ BddBelow s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Result:
case inl
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
hs : IsCompact ∅
⊢ BddBelow ∅

case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s

Proof state:
case inl
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
hs : IsCompact ∅
⊢ BddBelow ∅

Tactic:
exact bddBelow_empty

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s

Tactic:
obtain ⟨a, -, has⟩ := hs.exists_isLeast hne

Result:
case inr.intro.intro
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
a : α
has : a ∈ lowerBounds s
⊢ BddBelow s
-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem P3_of_lt {y₁ y₂} (h : ∀ i, IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂)
    (hs : ∀ i, IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂) (hl : x₁ < x₂) :
    P3 x₁ x₂ y₁ y₂

Proof state:
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
obtain (⟨i,hi⟩|⟨i,hi⟩) := lf_iff_exists_le.1 (lf_of_lt hl)

Result:
case inl.intro
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
i : x₂.LeftMoves
hi : x₁ ≤ x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂

case inr.intro
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
i : x₁.RightMoves
hi : x₁.moveRight i ≤ x₂
⊢ P3 x₁ x₂ y₁ y₂

Proof state:
case inr.intro
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
i : x₁.RightMoves
hi : x₁.moveRight i ≤ x₂
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
apply P3_neg.2 <| P3_of_le_left _ (hs (toLeftMovesNeg i)) _

Result:
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
i : x₁.RightMoves
hi : x₁.moveRight i ≤ x₂
⊢ -x₂ ≤ (-x₁).moveLeft (toLeftMovesNeg i)

Proof state:
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
i : x₁.RightMoves
hi : x₁.moveRight i ≤ x₂
⊢ -x₂ ≤ (-x₁).moveLeft (toLeftMovesNeg i)

Tactic:
simpa

Result:
no goals

Proof state:
case inl.intro
x₁ x₂ y₁ y₂ : PGame
h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂
hl : x₁ < x₂
i : x₂.LeftMoves
hi : x₁ ≤ x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
exact P3_of_le_left i (h i) hi

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- Exactness of `L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂`. -/
lemma L₂'_exact : S.L₂'.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₂'.Exact

Tactic:
rw [← exact_op_iff, exact_iff_of_iso S.L₂'OpIso]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.L₁'.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.L₁'.Exact

Tactic:
exact S.op.L₁'_exact

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem Subtype.preconnectedSpace {s : Set α} (h : IsPreconnected s) : PreconnectedSpace s where
  isPreconnected_univ

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ IsPreconnected univ

Tactic:
rwa [← IsInducing.subtypeVal.isPreconnected_image, image_univ, Subtype.range_val]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, the key factorization of `S'.a ^ 3 + S'.b ^ 3`. -/
lemma a_cube_add_b_cube_eq_mul :
    S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + η * S'.b) * (S'.a + η ^ 2 * S'.b)

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ S'.a ^ 3 + S'.a ^ 2 * S'.b * (↑η ^ 2 + ↑η + 1) + S'.a * S'.b ^ 2 * (↑η ^ 2 + ↑η + ↑η ^ 3) + ↑η ^ 3 * S'.b ^ 3 =
    S'.a ^ 3 + S'.a ^ 2 * S'.b * (↑η ^ 2 + ↑η + 1) + S'.a * S'.b ^ 2 * (↑η ^ 2 + ↑η + 1) + S'.b ^ 3

Tactic:
simp [hζ.toInteger_cube_eq_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + ↑η * S'.b) * (S'.a + ↑η ^ 2 * S'.b)

Tactic:
symm

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ (S'.a + S'.b) * (S'.a + ↑η * S'.b) * (S'.a + ↑η ^ 2 * S'.b) = S'.a ^ 3 + S'.b ^ 3

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ (S'.a + S'.b) * (S'.a + ↑η * S'.b) * (S'.a + ↑η ^ 2 * S'.b) = S'.a ^ 3 + S'.b ^ 3

Tactic:
calc _ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+η^3)+η^3*S'.b^3 := by ring
_ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+1)+S'.b^3 := by
  simp [hζ.toInteger_cube_eq_one]
_ = S'.a ^ 3 + S'.b ^ 3 := by rw [eta_sq]; ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ (S'.a + S'.b) * (S'.a + ↑η * S'.b) * (S'.a + ↑η ^ 2 * S'.b) =
    S'.a ^ 3 + S'.a ^ 2 * S'.b * (↑η ^ 2 + ↑η + 1) + S'.a * S'.b ^ 2 * (↑η ^ 2 + ↑η + ↑η ^ 3) + ↑η ^ 3 * S'.b ^ 3

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ S'.a ^ 3 + S'.a ^ 2 * S'.b * (↑η ^ 2 + ↑η + 1) + S'.a * S'.b ^ 2 * (↑η ^ 2 + ↑η + 1) + S'.b ^ 3 = S'.a ^ 3 + S'.b ^ 3

Tactic:
rw [eta_sq]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ S'.a ^ 3 + S'.a ^ 2 * S'.b * (-↑η - 1 + ↑η + 1) + S'.a * S'.b ^ 2 * (-↑η - 1 + ↑η + 1) + S'.b ^ 3 =
    S'.a ^ 3 + S'.b ^ 3

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
⊢ S'.a ^ 3 + S'.a ^ 2 * S'.b * (-↑η - 1 + ↑η + 1) + S'.a * S'.b ^ 2 * (-↑η - 1 + ↑η + 1) + S'.b ^ 3 =
    S'.a ^ 3 + S'.b ^ 3

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Localization.lean
@[simp, reassoc]
lemma iso_inv_app (a : A) (X : C) :
    (commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) =
        (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
        (F.commShiftIso a).inv.app X ≫
      (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫
      F'.map ((L.commShiftIso a).hom.app X)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (iso L W F F' a).inv.app (L.obj X) =
    (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
      (F.commShiftIso a).inv.app X ≫
        (Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X) ≫ F'.map ((L.commShiftIso a).hom.app X)

Tactic:
simp [commShiftOfLocalization.iso]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.rankPos_of_nonempty (hI : M.Indep I) (hne : I.Nonempty) : M.RankPos

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.RankPos

Tactic:
exact hB.rankPos_of_nonempty (hne.mono hIB)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
⊢ M.RankPos

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hne : I.Nonempty
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.RankPos
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma πFunctorObj_eq (j : κ.ord.toType) :
    letI := hasColimitsOfShape_discrete I κ
    letI := hasPushouts I κ
    πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
      (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
      πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
have h₁ := (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.w

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
h₁ :
  (𝟭 C).map (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))).right.hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app (Arrow.mk f))).right.hom ≫
      (𝟭 C).map (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.right
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEmpty_iff_size_eq_zero {l : Array α} : l.isEmpty ↔ l.size = 0

Proof state:
α : Type u_1
l : Array α
⊢ l.isEmpty = true ↔ l.size = 0

Tactic:
rw [isEmpty_iff, size_eq_zero]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem lim_im (f : CauSeq ℂ (‖·‖)) : lim (cauSeqIm f) = (lim f).im

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqIm f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).im

Tactic:
simp [ofReal]

Result:
no goals

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqIm f).lim = f.lim.im

Tactic:
rw [lim_eq_lim_im_add_lim_re]

Result:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqIm f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).im