harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem prod_Icc_factorial : ∀ n : ℕ, ∏ x ∈ Icc 1 n, x ! = sf n
  | 0 => rfl
  | n + 1 => by
    rw [← Ico_succ_right 1 n.succ, prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n,
    Nat.factorial_succ, Ico_succ_right 1 n, prod_Icc_factorial n, superFactorial, factorial,
    Nat.succ_eq_add_one, mul_comm]

Proof state:
n : ℕ
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1

Tactic:
rw [← Ico_succ_right 1 n.succ, prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n,
Nat.factorial_succ, Ico_succ_right 1 n, prod_Icc_factorial n, superFactorial, factorial,
Nat.succ_eq_add_one, mul_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_add_of_nonneg (x : ℝ≥0) {y z : ℝ} (hy : 0 ≤ y) (hz : 0 ≤ z) :
    x ^ (y + z) = x ^ y * x ^ z

Proof state:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
ext

Result:
case a
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ↑(x ^ (y + z)) = ↑(x ^ y * x ^ z)

Proof state:
case a
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ↑(x ^ (y + z)) = ↑(x ^ y * x ^ z)

Tactic:
exact Real.rpow_add_of_nonneg x.2 hy hz

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem coe_sumCoords_eq_finsum : (b.sumCoords : M → R) = fun m => ∑ᶠ i, b.coord i m

Proof state:
case h
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
m : M
⊢ b.sumCoords m = ∑ᶠ (i : ι), (b.coord i) m

Tactic:
simp only [Basis.sumCoords, Basis.coord, Finsupp.lapply_apply, LinearMap.id_coe,
  LinearEquiv.coe_coe, Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp,
  finsum_eq_sum _ (b.repr m).finite_support, Finsupp.sum, Finset.finite_toSet_toFinset, id,
  Finsupp.fun_support_eq]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ ⇑b.sumCoords = fun m => ∑ᶠ (i : ι), (b.coord i) m

Tactic:
ext m

Result:
case h
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
m : M
⊢ b.sumCoords m = ∑ᶠ (i : ι), (b.coord i) m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.mergeIdem_nonEmpty (e : List Nat) (h : e ≠ []) : mergeIdem e ≠ []

Proof state:
case single
a✝ : Nat
h : [a✝] ≠ []
⊢ mergeIdem [a✝] ≠ []

Tactic:
simp [mergeIdem, mergeIdem.loop]

Result:
no goals

Proof state:
e : List Nat
h : e ≠ []
⊢ mergeIdem e ≠ []

Tactic:
induction e using List.two_step_induction with
| empty => simp_all
| single => simp [mergeIdem, mergeIdem.loop]
| step => simp [mergeIdem, mergeIdem.loop] at *; split <;> simp_all

Result:
no goals

Proof state:
case empty
h : [] ≠ []
⊢ mergeIdem [] ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
case step
a✝¹ b✝ : Nat
l✝ : List Nat
a✝ : b✝ :: l✝ ≠ [] → mergeIdem (b✝ :: l✝) ≠ []
h : a✝¹ :: b✝ :: l✝ ≠ []
⊢ mergeIdem (a✝¹ :: b✝ :: l✝) ≠ []

Tactic:
simp [mergeIdem, mergeIdem.loop] at *

Result:
case step
a✝¹ b✝ : Nat
l✝ : List Nat
a✝ : ¬mergeIdem.loop b✝ l✝ = []
h : True
⊢ ¬(if a✝¹ = b✝ then mergeIdem.loop a✝¹ l✝ else a✝¹ :: mergeIdem.loop b✝ l✝) = []

Proof state:
case step
a✝¹ b✝ : Nat
l✝ : List Nat
a✝ : ¬mergeIdem.loop b✝ l✝ = []
h : True
⊢ ¬(if a✝¹ = b✝ then mergeIdem.loop a✝¹ l✝ else a✝¹ :: mergeIdem.loop b✝ l✝) = []

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_iff_multifork :
    IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))

Proof state:
case h.right.x.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I => x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b))) ≫
      (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
congr 1

Result:
case h.right.x.right.e_a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I => x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b)) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b))

Proof state:
case h.right.x.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I => x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)

Tactic:
rw [← K.w (WalkingMulticospan.Hom.fst b), ←
  (T.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]

Result:
case h.right.x.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I => x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b))) ≫
      (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_gt_d6 : 3.141592 < π

Proof state:
⊢ 3.141592 < π

Tactic:
pi_lower_bound [
  11482/8119, 7792/4217, 54055/27557, 2-623/64690, 2-337/139887, 2-208/345307, 2-167/1108925,
  2-64/1699893, 2-31/3293535, 2-48/20398657]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem sub : mapFun f (x - y) = mapFun f x - mapFun f y

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
⊢ mapFun (⇑f) (x - y) = mapFun (⇑f) x - mapFun (⇑f) y

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_sup : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g

Proof state:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ∅.sup (f ⊔ g) = ∅.sup f ⊔ ∅.sup g

Tactic:
rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]

Result:
no goals

Proof state:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (cons a✝ s✝ h✝).sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
rw [sup_cons, sup_cons, sup_cons, ih]

Result:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ (s✝.sup f ⊔ s✝.sup g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)

Proof state:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ (s✝.sup f ⊔ s✝.sup g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)

Tactic:
exact sup_sup_sup_comm _ _ _ _

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ s.sup (f ⊔ g) = s.sup f ⊔ s.sup g

Tactic:
induction s using Finset.cons_induction with
| empty => rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
| cons _ _ _ ih =>
  rw [sup_cons, sup_cons, sup_cons, ih]
  exact sup_sup_sup_comm _ _ _ _

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_lt_map {f : α → β} {s t : Multiset α} (h : s < t) : s.map f < t.map f

Proof state:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ s.card

Tactic:
rw [← s.card_map f, ← t.card_map f]

Result:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ (map f t).card ≤ (map f s).card

Proof state:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t

Tactic:
refine (map_le_map h.le).lt_of_not_le fun H => h.ne <| eq_of_le_of_card_le h.le ?_

Result:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ s.card

Proof state:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ (map f t).card ≤ (map f s).card

Tactic:
exact card_le_card H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_shiftLeft (x : Nat) : testBit (x <<< i) j =
    (decide (j ≥ i) && testBit x (j-i))

Proof state:
i j x : Nat
⊢ (x <<< i).testBit j = (decide (j ≥ i) && x.testBit (j - i))

Tactic:
simp [shiftLeft_eq, Nat.mul_comm _ (2^_), testBit_mul_pow_two]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ico_add_one_right_eq_Icc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ico a (b + 1) = Icc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc_of_not_isMax hb a

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem range_pullback_to_base_of_right :
    Set.range (pullback.fst g f ≫ g).base =
      Set.range g.base ∩ Set.range f.base

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.fst g f ≫ g).base) =
    Set.range ⇑(ConcreteCategory.hom g.base) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp, range_pullback_fst_of_right,
  Opens.map_obj, Opens.carrier_eq_coe, Opens.coe_mk, Set.image_preimage_eq_inter_range,
  Set.inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _

Proof state:
n : Nat
k : Fin (n + 2)
⊢ (↑k + ↑1) % (n + 2) < ↑k ↔ ↑k = n + 1

Tactic:
let ⟨k, hk⟩ := k

Result:
n : Nat
k✝ : Fin (n + 2)
k : Nat
hk : k < n + 2
⊢ (↑⟨k, hk⟩ + ↑1) % (n + 2) < ↑⟨k, hk⟩ ↔ ↑⟨k, hk⟩ = n + 1

Proof state:
n : Nat
k✝ : Fin (n + 2)
k : Nat
hk : k < n + 2
⊢ (↑⟨k, hk⟩ + ↑1) % (n + 2) < ↑⟨k, hk⟩ ↔ ↑⟨k, hk⟩ = n + 1

Tactic:
match Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hk) with
| .inl h => cases h; simp [Nat.succ_pos]
| .inr hk' => simp [Nat.ne_of_lt hk', Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.le_succ]

Result:
no goals

Proof state:
n : Nat
k✝ : Fin (n + 2)
k : Nat
hk : k < n + 2
h : k = n + 1
⊢ (↑⟨k, hk⟩ + ↑1) % (n + 2) < ↑⟨k, hk⟩ ↔ ↑⟨k, hk⟩ = n + 1

Tactic:
cases h

Result:
case refl
n : Nat
k : Fin (n + 2)
hk : n + 1 < n + 2
⊢ (↑⟨n + 1, hk⟩ + ↑1) % (n + 2) < ↑⟨n + 1, hk⟩ ↔ ↑⟨n + 1, hk⟩ = n + 1

Proof state:
n : Nat
k : Fin (n + 2)
⊢ k + 1 < k ↔ k = last (n + 1)

Tactic:
simp only [lt_def, val_add, val_last, Fin.ext_iff]

Result:
n : Nat
k : Fin (n + 2)
⊢ (↑k + ↑1) % (n + 2) < ↑k ↔ ↑k = n + 1

Proof state:
n : Nat
k✝ : Fin (n + 2)
k : Nat
hk : k < n + 2
hk' : k < n + 1
⊢ (↑⟨k, hk⟩ + ↑1) % (n + 2) < ↑⟨k, hk⟩ ↔ ↑⟨k, hk⟩ = n + 1

Tactic:
simp [Nat.ne_of_lt hk', Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.le_succ]

Result:
no goals

Proof state:
case refl
n : Nat
k : Fin (n + 2)
hk : n + 1 < n + 2
⊢ (↑⟨n + 1, hk⟩ + ↑1) % (n + 2) < ↑⟨n + 1, hk⟩ ↔ ↑⟨n + 1, hk⟩ = n + 1

Tactic:
simp [Nat.succ_pos]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc (attr := simp)]
lemma unit_app_commShiftIso_hom_app [adj.CommShift A] (a : A) (X : C) :
    adj.unit.app (X⟦a⟧) ≫ ((F ⋙ G).commShiftIso a).hom.app X = (adj.unit.app X)⟦a⟧'

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

Tactic:
simpa using (NatTrans.shift_app_comm adj.unit a X).symm

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsUniform.pos (hG : G.IsUniform ε s t) : 0 < ε :=
  not_le.1 fun hε ↦ (hε.trans <| abs_nonneg _).not_lt <| hG (empty_subset _) (empty_subset _)
    (by simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε)
    (by simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
hG : G.IsUniform ε s t
hε : ε ≤ 0
⊢ ↑(#s) * ε ≤ ↑(#∅)

Tactic:
simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
hG : G.IsUniform ε s t
hε : ε ≤ 0
⊢ ↑(#t) * ε ≤ ↑(#∅)

Tactic:
simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit
    {ι : Type u} (f : ι → Cardinal.{v}) (ω : Cardinal.{v})
    (hω : ¬ IsSuccPrelimit ω)
    (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω

Proof state:
ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit (⨆ i, f i)
⊢ BddAbove (range f)

Tactic:
contrapose! hω with hf

Result:
ι : Type u
f : ι → Cardinal.{v}
hf : ¬BddAbove (range f)
⊢ IsSuccPrelimit (⨆ i, f i)

Proof state:
ι : Type u
f : ι → Cardinal.{v}
hf : ¬BddAbove (range f)
⊢ IsSuccPrelimit ⊥

Tactic:
exact isSuccPrelimit_bot

Result:
no goals

Proof state:
ι : Type u
f : ι → Cardinal.{v}
hf : ¬BddAbove (range f)
⊢ IsSuccPrelimit (⨆ i, f i)

Tactic:
rw [iSup, csSup_of_not_bddAbove hf, csSup_empty]

Result:
ι : Type u
f : ι → Cardinal.{v}
hf : ¬BddAbove (range f)
⊢ IsSuccPrelimit ⊥

Proof state:
ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit (⨆ i, f i)
⊢ ∃ i, f i = ⨆ i, f i

Tactic:
suffices BddAbove (range f) from (isLUB_csSup' this).mem_of_not_isSuccPrelimit hω

Result:
ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit (⨆ i, f i)
⊢ BddAbove (range f)

Proof state:
ι : Type u
f : ι → Cardinal.{v}
ω : Cardinal.{v}
hω : ¬IsSuccPrelimit ω
h : ⨆ i, f i = ω
⊢ ∃ i, f i = ω

Tactic:
subst h

Result:
ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit (⨆ i, f i)
⊢ ∃ i, f i = ⨆ i, f i
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
@[simp]
lemma LinearMap.toMatrix_singleton {ι : Type*} [Unique ι] (f : R →ₗ[R] R) (i j : ι) :
    f.toMatrix (.singleton ι R) (.singleton ι R) i j = f 1

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_7
inst✝ : Unique ι
f : R →ₗ[R] R
i j : ι
⊢ (toMatrix (Basis.singleton ι R) (Basis.singleton ι R)) f i j = f 1

Tactic:
simp [toMatrix, Subsingleton.elim j default]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dZero_comp_eq : dZero A ∘ₗ (zeroCochainsLequiv A) =
    oneCochainsLequiv A ∘ₗ ((inhomogeneousCochains A).d 0 1).hom

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 0)
y : G
⊢ (A.ρ y) (x default) - x default =
    (A.ρ ((Equiv.funUnique (Fin 1) G).symm y 0)) (x fun i => (Equiv.funUnique (Fin 1) G).symm y i.succ) +
      ∑ j ∈ {0}, (-1) ^ (↑j + 1) • x (j.contractNth (fun x1 x2 => x1 * x2) ((Equiv.funUnique (Fin 1) G).symm y))

Tactic:
simp_rw [Fin.val_eq_zero, zero_add, pow_one, neg_smul, one_smul,
  Finset.sum_singleton, sub_eq_add_neg]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 0)
y : G
⊢ (A.ρ y) (x default) + -x default =
    (A.ρ ((Equiv.funUnique (Fin 1) G).symm y 0)) (x fun i => (Equiv.funUnique (Fin 1) G).symm y i.succ) +
      -x (Fin.contractNth 0 (fun x1 x2 => x1 * x2) ((Equiv.funUnique (Fin 1) G).symm y))

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 0)
y : G
⊢ (dZero A ∘ₗ ↑(zeroCochainsLequiv A)) x y =
    (↑(oneCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1)) x y

Tactic:
show A.ρ y (x default) - x default = _ + ({0} : Finset _).sum _

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 0)
y : G
⊢ (A.ρ y) (x default) - x default =
    (A.ρ ((Equiv.funUnique (Fin 1) G).symm y 0)) (x fun i => (Equiv.funUnique (Fin 1) G).symm y i.succ) +
      ∑ j ∈ {0}, (-1) ^ (↑j + 1) • x (j.contractNth (fun x1 x2 => x1 * x2) ((Equiv.funUnique (Fin 1) G).symm y))

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ dZero A ∘ₗ ↑(zeroCochainsLequiv A) = ↑(oneCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1)

Tactic:
ext x y

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 0)
y : G
⊢ (dZero A ∘ₗ ↑(zeroCochainsLequiv A)) x y =
    (↑(oneCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1)) x y

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 0)
y : G
⊢ (A.ρ y) (x default) + -x default =
    (A.ρ ((Equiv.funUnique (Fin 1) G).symm y 0)) (x fun i => (Equiv.funUnique (Fin 1) G).symm y i.succ) +
      -x (Fin.contractNth 0 (fun x1 x2 => x1 * x2) ((Equiv.funUnique (Fin 1) G).symm y))

Tactic:
rcongr i <;> exact Fin.elim0 i

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq_integral_pos_part_sub_integral_neg_part {f : α → ℝ} (hf : Integrable f μ) :
    ∫ a, f a ∂μ = ∫ a, (Real.toNNReal (f a) : ℝ) ∂μ - ∫ a, (Real.toNNReal (-f a) : ℝ) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun a => ↑(-f a).toNNReal) μ

Tactic:
exact hf.neg.real_toNNReal

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ

Tactic:
rw [← integral_sub hf.real_toNNReal]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal - ↑(-f a).toNNReal ∂μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun a => ↑(-f a).toNNReal) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal - ↑(-f a).toNNReal ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem not_sat_of_isImpossible (h : isImpossible c) {t} : ¬ c.sat t

Proof state:
case mk.some.some
t l u : Int
h : u < l
w : l ≤ t
⊢ u < t

Tactic:
exact Int.lt_of_lt_of_le h w

Result:
no goals

Proof state:
c : Constraint
h : c.isImpossible = true
t : Int
⊢ ¬c.sat t = true

Tactic:
rcases c with ⟨_ | l, _ | u⟩ <;> simp [isImpossible, sat] at h ⊢

Result:
case mk.some.some
t l u : Int
h : u < l
⊢ l ≤ t → ¬t ≤ u

Proof state:
case mk.some.some
t l u : Int
h : u < l
⊢ l ≤ t → ¬t ≤ u

Tactic:
intro w

Result:
case mk.some.some
t l u : Int
h : u < l
w : l ≤ t
⊢ ¬t ≤ u

Proof state:
case mk.some.some
t l u : Int
h : u < l
w : l ≤ t
⊢ ¬t ≤ u

Tactic:
rw [Int.not_le]

Result:
case mk.some.some
t l u : Int
h : u < l
w : l ≤ t
⊢ u < t
-- Mathlib/Order/Height.lean
theorem chainHeight_eq_zero_iff : s.chainHeight = 0 ↔ s = ∅

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
⊢ s.chainHeight = 0 ↔ s = ∅

Tactic:
rw [← not_iff_not, ← Ne, ← ENat.one_le_iff_ne_zero, one_le_chainHeight_iff,
  nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
@[simp]
lemma map_prodComm_divisorsAntidiag :
    z.divisorsAntidiag.map (Equiv.prodComm _ _).toEmbedding = z.divisorsAntidiag

Proof state:
z : ℤ
⊢ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
ext

Result:
case h
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag

Proof state:
case h
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag, mul_comm]

Result:
no goals