harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Chain.lean
theorem IsChain.succ (hs : IsChain r s) : IsChain r (SuccChain r s) :=
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then (succChain_spec h).1
  else by
    rw [exists_and_left] at h
    simpa [SuccChain, dif_neg, h] using hs

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)

Tactic:
simpa [SuccChain, dif_neg, h] using hs

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)

Tactic:
rw [exists_and_left] at h

Result:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
-- Mathlib/Topology/Algebra/Support.lean
theorem LocallyFinite.exists_finset_nhd_mulSupport_subset {U : ι → Set X} [One R] {f : ι → X → R}
    (hlf : LocallyFinite fun i => mulSupport (f i)) (hso : ∀ i, mulTSupport (f i) ⊆ U i)
    (ho : ∀ i, IsOpen (U i)) (x : X) :
    ∃ (is : Finset ι), ∃ n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ i ∈ is, U i) ∧
      ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ is

Proof state:
case intro.intro.refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑hnf.toFinset

Tactic:
intro i hi

Result:
case intro.intro.refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ i ∈ ↑hnf.toFinset
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_swap' {x y : α} : sign (swap x y) = if x = y then 1 else -1 :=
  if H : x = y then by simp [H, swap_self] else by simp [sign_swap H, H]

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
H : ¬x = y
⊢ sign (swap x y) = if x = y then 1 else -1

Tactic:
simp [sign_swap H, H]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
H : x = y
⊢ sign (swap x y) = if x = y then 1 else -1

Tactic:
simp [H, swap_self]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem Sum.dist_comm (x y : X ⊕ Y) : Sum.dist x y = Sum.dist y x

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x y : X ⊕ Y
⊢ Sum.dist x y = Sum.dist y x

Tactic:
cases x <;> cases y <;> simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm, add_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma iteratedFDeriv_aux {ι} {M₁ : ι → Type*} {α : Type*} [DecidableEq α]
    (s : Set ι) [DecidableEq { x // x ∈ s }] (e : α ≃ s)
    (m : α → ((i : ι) → M₁ i)) (a : α) (z : (i : ι) → M₁ i) :
    (fun i ↦ update m a z (e.symm i) i) =
      (fun i ↦ update (fun j ↦ m (e.symm j) j) (e a) (z (e a)) i)

Proof state:
case h.inr
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
hne : a ≠ e.symm i
⊢ update m a z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]

Result:
no goals

Proof state:
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
⊢ (fun i => update m a z (e.symm i) ↑i) = fun i => update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
ext i

Result:
case h
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
⊢ update m a z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Proof state:
case h
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
⊢ update m a z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
rcases eq_or_ne a (e.symm i) with rfl | hne

Result:
case h.inl
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
z : (i : ι) → M₁ i
i : ↑s
⊢ update m (e.symm i) z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e (e.symm i)) (z ↑(e (e.symm i))) i

case h.inr
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
hne : a ≠ e.symm i
⊢ update m a z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Proof state:
case h.inl
ι : Type u_4
M₁ : ι → Type u_2
α : Type u_3
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
z : (i : ι) → M₁ i
i : ↑s
⊢ update m (e.symm i) z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e (e.symm i)) (z ↑(e (e.symm i))) i

Tactic:
rw [Equiv.apply_symm_apply e i, update_self, update_self]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
@[reassoc]
lemma homRestrict_precomp (α : K' ⟶ K) (ψ : K ⟶ L.extend e) :
    e.homRestrict (α ≫ ψ) = restrictionMap α e ≫ e.homRestrict ψ

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
⊢ e.homRestrict (α ≫ ψ) = restrictionMap α e ≫ e.homRestrict ψ

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
i : ι
⊢ (e.homRestrict (α ≫ ψ)).f i = (restrictionMap α e ≫ e.homRestrict ψ).f i

Proof state:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
i : ι
⊢ (e.homRestrict (α ≫ ψ)).f i = (restrictionMap α e ≫ e.homRestrict ψ).f i

Tactic:
simp [homRestrict_f _ _ rfl, restrictionXIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_eq_zero_of_left_eq_zero {xs ys : IntList} (h : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0

Proof state:
case nil
ys : IntList
h : ∀ (x : Int), x ∈ [] → x = 0
⊢ dot [] ys = 0

Tactic:
rfl

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
h : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ dot (x :: xs) (y :: ys) = 0

Tactic:
rw [dot_cons₂, h x (List.mem_cons_self _ _), ih (fun x m => h x (List.mem_cons_of_mem _ m)),
  Int.zero_mul, Int.add_zero]

Result:
no goals

Proof state:
case cons.nil
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
h : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
⊢ dot (x :: xs) [] = 0

Tactic:
rfl

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
ys : IntList
h : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
⊢ dot (x :: xs) ys = 0

Tactic:
cases ys with
| nil => rfl
| cons y ys =>
  rw [dot_cons₂, h x (List.mem_cons_self _ _), ih (fun x m => h x (List.mem_cons_of_mem _ m)),
    Int.zero_mul, Int.add_zero]

Result:
no goals

Proof state:
xs ys : IntList
h : ∀ (x : Int), x ∈ xs → x = 0
⊢ xs.dot ys = 0

Tactic:
induction xs generalizing ys with
| nil => rfl
| cons x xs ih =>
  cases ys with
  | nil => rfl
  | cons y ys =>
    rw [dot_cons₂, h x (List.mem_cons_self _ _), ih (fun x m => h x (List.mem_cons_of_mem _ m)),
      Int.zero_mul, Int.add_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_right_Icc (a b c : α) : (Icc a b).image (· + c) = Icc (a + c) (b + c)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
rw [← map_add_right_Icc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_eq_iff (p : ℕ) (n : ℕ) (z : ZMod p) [NeZero p] :
    ↑n = z ↔ ∃ k, n = z.val + p * k

Proof state:
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑(z.val + p * k) = z

Tactic:
rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
  add_zero]

Result:
no goals

Proof state:
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = z.val + p * k

Tactic:
constructor

Result:
case mp
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = z.val + p * k

case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = z.val + p * k) → ↑n = z

Proof state:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = (↑n).val + p * (n / p)

Tactic:
rw [val_natCast, Nat.mod_add_div]

Result:
no goals

Proof state:
case mp
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = z.val + p * k

Tactic:
rintro rfl

Result:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ ∃ k, n = (↑n).val + p * k

Proof state:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ ∃ k, n = (↑n).val + p * k

Tactic:
refine ⟨n / p, ?_⟩

Result:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = (↑n).val + p * (n / p)

Proof state:
case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = z.val + p * k) → ↑n = z

Tactic:
rintro ⟨k, rfl⟩

Result:
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑(z.val + p * k) = z
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem germ_res_apply' (F : X.Presheaf C)
    {U V : Opens X} (i : op V ⟶ op U) (x : X) (hx : x ∈ U) [ConcreteCategory C FC] (s) :
    F.germ U x hx (F.map i s) = F.germ V x (i.unop.le hx) s

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens ↑X
i : op V ⟶ op U
x : ↑X
hx : x ∈ U
inst✝ : ConcreteCategory C FC
s : CC (F.obj (op V))
⊢ (ConcreteCategory.hom (F.germ U x hx)) ((ConcreteCategory.hom (F.map i)) s) = (ConcreteCategory.hom (F.germ V x ⋯)) s

Tactic:
rw [← ConcreteCategory.comp_apply, germ_res']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) :
    dfoldl n (fun _ => α) f x = foldl n (fun x i => f i x) x

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), dfoldl n (fun x => α) f x = foldl n (fun x i => f i x) x
f : Fin (n + 1) → α → α
x : α
⊢ dfoldl (n + 1) (fun x => α) f x = foldl (n + 1) (fun x i => f i x) x

Tactic:
simp only [dfoldl_succ, foldl_succ, Function.comp_apply, Function.comp_def]

Result:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), dfoldl n (fun x => α) f x = foldl n (fun x i => f i x) x
f : Fin (n + 1) → α → α
x : α
⊢ dfoldl n (fun x => α) (fun x1 x2 => f x1.succ x2) (f 0 x) = foldl n (fun x i => f i.succ x) (f 0 x)

Proof state:
case zero
α : Type u_1
f : Fin 0 → α → α
x : α
⊢ dfoldl 0 (fun x => α) f x = foldl 0 (fun x i => f i x) x

Tactic:
simp only [dfoldl_zero, foldl_zero]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α → α
x : α
⊢ dfoldl n (fun x => α) f x = foldl n (fun x i => f i x) x

Tactic:
induction n generalizing x with
| zero => simp only [dfoldl_zero, foldl_zero]
| succ n ih =>
  simp only [dfoldl_succ, foldl_succ, Function.comp_apply, Function.comp_def]
  congr; simp only [ih]

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), dfoldl n (fun x => α) f x = foldl n (fun x i => f i x) x
f : Fin (n + 1) → α → α
x : α
⊢ dfoldl n (fun x => α) (fun x1 x2 => f x1.succ x2) (f 0 x) = foldl n (fun x i => f i.succ x) (f 0 x)

Tactic:
simp only [ih]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem nonarchimedean {q r : ℚ} :
    padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

Tactic:
exact nonarchimedean_aux hle

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

Tactic:
rw [add_comm, max_comm]

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ padicNorm p r ⊔ padicNorm p q

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

Tactic:
wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ padicNorm p r ⊔ padicNorm p q

Tactic:
exact this (le_of_not_le hle)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem univ_inaccessible : IsInaccessible univ.{u, v} :=
  IsInaccessible.mk (by simpa using lift_lt_univ' ℵ₀) (by simp) fun c h => by
    rcases lt_univ'.1 h with ⟨c, rfl⟩
    rw [← lift_two_power]
    apply lift_lt_univ'

Proof state:
⊢ univ.{u, v} ≤ univ.{u, v}.ord.cof

Tactic:
simp

Result:
no goals

Proof state:
case intro
c : Cardinal.{u}
h : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ 2 ^ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
rw [← lift_two_power]

Result:
case intro
c : Cardinal.{u}
h : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} (2 ^ c) < univ.{u, v}

Proof state:
⊢ ℵ₀ < univ.{u, v}

Tactic:
simpa using lift_lt_univ' ℵ₀

Result:
no goals

Proof state:
case intro
c : Cardinal.{u}
h : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} (2 ^ c) < univ.{u, v}

Tactic:
apply lift_lt_univ'

Result:
no goals

Proof state:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
⊢ 2 ^ c < univ.{u, v}

Tactic:
rcases lt_univ'.1 h with ⟨c, rfl⟩

Result:
case intro
c : Cardinal.{u}
h : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ 2 ^ lift.{max (u + 1) v, u} c < univ.{u, v}
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem Commute.mul_zpow {A B : M} (h : Commute A B) : ∀ i : ℤ, (A * B) ^ i = A ^ i * B ^ i
  | (n : ℕ) => by simp [h.mul_pow n]
  | -[n+1] => by
    rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev,
      h.mul_pow n.succ, (h.pow_pow _ _).eq]

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ ↑n = A ^ ↑n * B ^ ↑n

Tactic:
simp [h.mul_pow n]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev,
  h.mul_pow n.succ, (h.pow_pow _ _).eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as

Proof state:
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin as✝.length
a : α
as : List α
i : Nat
h : i + 1 < (a :: as).length
ih : sizeOf (as.get ⟨i, ⋯⟩) < sizeOf as
⊢ sizeOf as < sizeOf (a :: as)

Tactic:
simp_arith

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin as.length
⊢ sizeOf (as.get i) < sizeOf as

Tactic:
match as, i with
| a::as, ⟨0, _⟩  => simp_arith [get]
| a::as, ⟨i+1, h⟩ =>
  have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
  apply Nat.lt_trans ih
  simp_arith

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i : Fin as✝.length
a : α
as : List α
isLt✝ : 0 < (a :: as).length
⊢ sizeOf ((a :: as).get ⟨0, isLt✝⟩) < sizeOf (a :: as)

Tactic:
simp_arith [get]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin as✝.length
a : α
as : List α
i : Nat
h : i + 1 < (a :: as).length
⊢ sizeOf ((a :: as).get ⟨i + 1, h⟩) < sizeOf (a :: as)

Tactic:
have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩

Result:
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin as✝.length
a : α
as : List α
i : Nat
h : i + 1 < (a :: as).length
ih : sizeOf (as.get ⟨i, ⋯⟩) < sizeOf as
⊢ sizeOf ((a :: as).get ⟨i + 1, h⟩) < sizeOf (a :: as)

Proof state:
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin as✝.length
a : α
as : List α
i : Nat
h : i + 1 < (a :: as).length
ih : sizeOf (as.get ⟨i, ⋯⟩) < sizeOf as
⊢ sizeOf ((a :: as).get ⟨i + 1, h⟩) < sizeOf (a :: as)

Tactic:
apply Nat.lt_trans ih

Result:
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin as✝.length
a : α
as : List α
i : Nat
h : i + 1 < (a :: as).length
ih : sizeOf (as.get ⟨i, ⋯⟩) < sizeOf as
⊢ sizeOf as < sizeOf (a :: as)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z = Q x * P z) :
    W'.negAddY P Q * (P z * Q z) ^ 2 = (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ W'.negAddY P Q * (P z * Q z) ^ 2 = (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Tactic:
rw [negAddY_eq' hP hQ, hx]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
              Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
            Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2) +
      P y * Q z * (Q x * P z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
              Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
            Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2) +
      P y * Q z * (Q x * P z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_pred_lt {a : Fin (n + 1)} (ha : a ≠ 0) :
    castSucc (a.pred ha) < a

Proof state:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < a

Tactic:
rw [castSucc_pred_lt_iff, le_def]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem erase_mem_compression (hs : s ∈ 𝒜) : s.erase a ∈ 𝓓 a 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
refine (em _).imp_right fun h => ⟨h, ?_⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : s.erase a ∉ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : s.erase a ∉ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝓓 a 𝒜

Tactic:
simp_rw [mem_compression, erase_idem, and_self_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty

Proof state:
α : Type u_1
inst✝ : BEq α
xs : Array α
⊢ (xs == #[]) = xs.isEmpty

Tactic:
cases xs

Result:
case mk
α : Type u_1
inst✝ : BEq α
toList✝ : List α
⊢ ({ toList := toList✝ } == #[]) = { toList := toList✝ }.isEmpty

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
toList✝ : List α
⊢ ({ toList := toList✝ } == #[]) = { toList := toList✝ }.isEmpty

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem continuousMap_mem_subalgebra_closure_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ))
    (w : A.SeparatesPoints) (f : C(X, ℝ)) : f ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ A.topologicalClosure

Tactic:
rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ ⊤