harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem toFinsupp_smul {S : Type*} [SMulZeroClass S k] (a : S) (b : SkewMonoidAlgebra k G) :
    (a • b).toFinsupp = a • b.toFinsupp

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
a : S
b : SkewMonoidAlgebra k G
⊢ (a • b).toFinsupp = a • b.toFinsupp

Tactic:
rw [← ofFinsupp_smul]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
lemma sum_collapse (h𝒜 : 𝒜 ⊆ (insert a u).powerset) (hu : a ∉ u) :
    ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s

Proof state:
case calc_2.e_a.e_s.e_a.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u

Tactic:
refine ⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩

Result:
case calc_2.e_a.e_s.e_a.h.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) → s.erase a ⊆ u ∧ ¬s ⊆ u

case calc_2.e_a.e_s.e_a.h.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
⊢ insert a (s.erase a) = s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False

Tactic:
rw [hs] at h

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem copy_cons {u v w u' w'} (h : G.Adj u v) (p : G.Walk v w) (hu : u = u') (hw : w = w') :
    (Walk.cons h p).copy hu hw = Walk.cons (hu ▸ h) (p.copy rfl hw)

Proof state:
V : Type u
G : SimpleGraph V
u v w u' w' : V
h : G.Adj u v
p : G.Walk v w
hu : u = u'
hw : w = w'
⊢ (cons h p).copy hu hw = cons ⋯ (p.copy ⋯ hw)

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
v u' w' : V
h : G.Adj u' v
p : G.Walk v w'
⊢ (cons h p).copy ⋯ ⋯ = cons ⋯ (p.copy ⋯ ⋯)

Proof state:
V : Type u
G : SimpleGraph V
v u' w' : V
h : G.Adj u' v
p : G.Walk v w'
⊢ (cons h p).copy ⋯ ⋯ = cons ⋯ (p.copy ⋯ ⋯)

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation_oangle_left (x y : V) : o.oangle (o.rotation (o.oangle x y) x) y = 0

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
simp [hy]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
by_cases hy : y = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
simp [hx, hy]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem isPathConnected_range [PathConnectedSpace X] {f : X → Y} (hf : Continuous f) :
    IsPathConnected (range f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous f
⊢ IsPathConnected (f '' univ)

Tactic:
exact isPathConnected_univ.image hf

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous f
⊢ IsPathConnected (range f)

Tactic:
rw [← image_univ]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous f
⊢ IsPathConnected (f '' univ)
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_singleton_eq_bot : (R ∙ x) = ⊥ ↔ x = 0 :=
  span_eq_bot.trans <| by simp

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (∀ x_1 ∈ {x}, x_1 = 0) ↔ x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem natCast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal)
  | 0 => by simp
  | n + 1 => by
    rw [pow_succ, natCast_mul, natCast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ]

Proof state:
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ ↑(n + 1)

Tactic:
rw [pow_succ, natCast_mul, natCast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ]

Result:
no goals

Proof state:
m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_inv_pos {α} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} :
    IsRat a (.ofNat (Nat.succ n)) d → IsRat a⁻¹ (.ofNat d) (Nat.succ n)

Proof state:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat n.succ) d → IsRat a⁻¹ (Int.ofNat d) n.succ

Tactic:
rintro ⟨_, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ

Proof state:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ = ↑(Int.ofNat d) * ⅟↑n.succ

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))

Result:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ

Proof state:
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ

Tactic:
exact ⟨this, by simp⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_left_inj {a b d : Int}
    (hda : d ∣ a) (hdb : d ∣ b) : a.tdiv d = b.tdiv d ↔ a = b

Proof state:
a b d : Int
hda : d ∣ a
hdb : d ∣ b
h : a.tdiv d = b.tdiv d
⊢ a = b

Tactic:
rw [← Int.mul_tdiv_cancel' hda, ← Int.mul_tdiv_cancel' hdb, h]

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean
theorem dist_birkhoffAverage_apply_birkhoffAverage (f : α → α) (g : α → E) (n : ℕ) (x : α) :
    dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) =
      dist (g (f^[n] x)) (g x) / n

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → α
g : α → E
n : ℕ
x : α
⊢ dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / ↑n

Tactic:
simp [dist_birkhoffAverage_birkhoffAverage, dist_birkhoffSum_apply_birkhoffSum]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) :
    X.presheaf.map i ≫ H.invApp _ (unop V) =
      invApp f (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (i ≫ eqToHom ⋯) =
    X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
rw [IsIso.comp_inv_eq]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))

Tactic:
simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
  NatTrans.naturality, Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc,
  TopCat.Presheaf.pushforward_obj_map]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (i ≫ eqToHom ⋯) =
    X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
simp only [invApp, ← Category.assoc]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_le (f : ℕ → Ω → ℝ) (ω : Ω) (hab : a < b) :
    upcrossingsBefore a b f N ω ≤ N

Proof state:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f 0 ω ≤ 0

Tactic:
rw [upcrossingsBefore_zero]

Result:
no goals

Proof state:
case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ N

Tactic:
by_contra hnN

Result:
case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hnN : ¬n ≤ N
⊢ False

Proof state:
case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
refine csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => ?_

Result:
case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ N

Proof state:
case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hnN : ¬n ≤ N
⊢ False

Tactic:
exact hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)

Result:
no goals

Proof state:
case pos
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
subst hN

Result:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f 0 ω ≤ 0

Proof state:
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
by_cases hN : N = 0

Result:
case pos
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω ≤ N

case neg
Ω : Type u_1
a b : ℝ
N : ℕ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma isLUB_range_ωSup (c : Chain α) : IsLUB (Set.range c) (ωSup c)

Proof state:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (a : ℕ), c a ≤ ωSup c

Tactic:
exact fun a ↦ le_ωSup c a

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsLUB (Set.range ⇑c) (ωSup c)

Tactic:
constructor

Result:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ upperBounds (Set.range ⇑c)

case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Proof state:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Tactic:
simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
  forall_apply_eq_imp_iff, Set.mem_setOf_eq]

Result:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), c a_1 ≤ a) → ωSup c ≤ a

Proof state:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), c a_1 ≤ a) → ωSup c ≤ a

Tactic:
exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Result:
no goals

Proof state:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ upperBounds (Set.range ⇑c)

Tactic:
simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
  Set.mem_setOf_eq]

Result:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (a : ℕ), c a ≤ ωSup c
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_left_one : (a * ·) ⁻¹' 1 = {a⁻¹}

Proof state:
α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x => a * x) ⁻¹' 1 = {a⁻¹}

Tactic:
rw [← image_mul_left', image_one, mul_one]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.pow (p : ℕ) (hf : GrowsPolynomially f)
    (hf_nonneg : ∀ᶠ x in atTop, 0 ≤ f x) : GrowsPolynomially fun x => (f x) ^ p

Proof state:
f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x ^ ↑p

Tactic:
exact hf.rpow p hf_nonneg

Result:
no goals

Proof state:
f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x ^ p

Tactic:
simp_rw [← rpow_natCast]

Result:
f : ℝ → ℝ
p : ℕ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x ^ ↑p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_append_of_length_le {l : Array α} {k : Nat} (hk : l.size ≤ k) (l' : Array α) (h) :
    eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - l.size) (by simp at h; omega)

Proof state:
case mk
α : Type u_1
k : Nat
l' : Array α
l : List α
hk : { toList := l }.size ≤ k
h : k < ({ toList := l } ++ l').size
⊢ ({ toList := l } ++ l').eraseIdx k h = { toList := l } ++ l'.eraseIdx (k - { toList := l }.size) ⋯

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk : { toList := l }.size ≤ k
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h =
    { toList := l } ++ { toList := l' }.eraseIdx (k - { toList := l }.size) ⋯

Proof state:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk : { toList := l }.size ≤ k
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h =
    { toList := l } ++ { toList := l' }.eraseIdx (k - { toList := l }.size) ⋯

Tactic:
simp at hk

Result:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk✝ : { toList := l }.size ≤ k
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
hk : l.length ≤ k
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h =
    { toList := l } ++ { toList := l' }.eraseIdx (k - { toList := l }.size) ⋯

Proof state:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk✝ : { toList := l }.size ≤ k
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
hk : l.length ≤ k
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h =
    { toList := l } ++ { toList := l' }.eraseIdx (k - { toList := l }.size) ⋯

Tactic:
simp [List.eraseIdx_append_of_length_le, *]

Result:
no goals

Proof state:
α : Type u_1
l : Array α
k : Nat
hk : l.size ≤ k
l' : Array α
h : k < (l ++ l').size
⊢ (l ++ l').eraseIdx k h = l ++ l'.eraseIdx (k - l.size) ⋯

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
k : Nat
l' : Array α
l : List α
hk : { toList := l }.size ≤ k
h : k < ({ toList := l } ++ l').size
⊢ ({ toList := l } ++ l').eraseIdx k h = { toList := l } ++ l'.eraseIdx (k - { toList := l }.size) ⋯

Proof state:
α : Type ?u.56755
l : Array α
k : Nat
hk : l.size ≤ k
l' : Array α
h : k < l.size + l'.size
⊢ k - l.size < l'.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.56755
l : Array α
k : Nat
hk : l.size ≤ k
l' : Array α
h : k < (l ++ l').size
⊢ k - l.size < l'.size

Tactic:
simp at h

Result:
α : Type ?u.56755
l : Array α
k : Nat
hk : l.size ≤ k
l' : Array α
h : k < l.size + l'.size
⊢ k - l.size < l'.size
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_of_finite (s : Set A)
    (H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R ((↑) : t → A)) :
    AlgebraicIndependent R ((↑) : s → A) :=
  algebraicIndependent_subtype.2 fun p hp ↦
    algebraicIndependent_subtype.1 (H _ (mem_supported.1 hp) (Finset.finite_toSet _)) _ (by simp)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val
p : MvPolynomial A R
hp : p ∈ supported R s
⊢ p ∈ supported R ↑p.vars

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/ENatENNReal.lean
@[simp, norm_cast]
lemma toENNReal_lt_top : (n : ℝ≥0∞) < ∞ ↔ n < ⊤

Proof state:
n : ℕ∞
⊢ ↑n < ⊤ ↔ n < ⊤

Tactic:
simp [← toENNReal_lt]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem of_think_mem {s : Computation α} {a} : a ∈ think s → a ∈ s
  | ⟨n, h⟩ => by
    rcases n with - | n'
    · contradiction
    · exact ⟨n', h⟩

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : (fun b => some a = b) ((↑s.think).get n)
⊢ a ∈ s

Tactic:
rcases n with - | n'

Result:
case zero
α : Type u
s : Computation α
a : α
h : some a = (↑s.think).get 0
⊢ a ∈ s

case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = (↑s.think).get (n' + 1)
⊢ a ∈ s

Proof state:
case zero
α : Type u
s : Computation α
a : α
h : some a = (↑s.think).get 0
⊢ a ∈ s

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = (↑s.think).get (n' + 1)
⊢ a ∈ s

Tactic:
exact ⟨n', h⟩

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_prod_of_regular {ι : Type*}
    {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) :
    m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Proof state:
case inr.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ ∏ i ∈ s, m.leadingCoeff (P i) ≠ 0

Tactic:
exact (IsRegular.prod H).ne_zero

Result:
no goals

Proof state:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
apply m.toSyn.injective

Result:
case inr.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ m.toSyn (m.degree (∏ i ∈ s, P i)) = m.toSyn (∑ i ∈ s, m.degree (P i))

Proof state:
case inr.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ ∑ i ∈ s, m.degree (P i) ∈ (∏ i ∈ s, P i).support

Tactic:
rw [mem_support_iff, m.coeff_prod_sum_degree]

Result:
case inr.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ ∏ i ∈ s, m.leadingCoeff (P i) ≠ 0

Proof state:
case inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Subsingleton R
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]

Result:
no goals

Proof state:
case inr.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ m.toSyn (m.degree (∏ i ∈ s, P i)) = m.toSyn (∑ i ∈ s, m.degree (P i))

Tactic:
refine le_antisymm degree_prod_le (m.le_degree ?_)

Result:
case inr.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h✝ : Nontrivial R
⊢ ∑ i ∈ s, m.degree (P i) ∈ (∏ i ∈ s, P i).support

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
cases subsingleton_or_nontrivial R with
| inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
| inr _ =>
  apply m.toSyn.injective
  refine le_antisymm degree_prod_le (m.le_degree ?_)
  rw [mem_support_iff, m.coeff_prod_sum_degree]
  exact (IsRegular.prod H).ne_zero

Result:
no goals