harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
/-- If `F` preserves the initial object and binary coproducts, then it preserves colimits of shape
`Discrete (Fin n)`.
-/
lemma preservesShape_fin_of_preserves_binary_and_initial (n : ℕ) :
    PreservesColimitsOfShape (Discrete (Fin n)) F where
  preservesColimit {K}

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ PreservesColimit K F

Tactic:
haveI := preserves_fin_of_preserves_binary_and_initial F n fun n => K.obj ⟨n⟩

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
this : PreservesColimit (Discrete.functor fun n_1 => K.obj { as := n_1 }) F
⊢ PreservesColimit K F

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
this : PreservesColimit (Discrete.functor fun n_1 => K.obj { as := n_1 }) F
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_iso_diagram F that

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ PreservesColimit K F

Tactic:
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ PreservesColimit K F
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_right_eq_add (a b c : α) :
    toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

Tactic:
simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem zero_mem_invSet (a : Nimber) : 0 ∈ invSet a

Proof state:
a : Nimber
⊢ 0 ∈ a.invSet

Tactic:
rw [invSet]

Result:
a : Nimber
⊢ 0 ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}

Proof state:
a : Nimber
⊢ 0 ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}

Tactic:
exact Set.mem_sInter.2 fun _ hs => hs.1

Result:
no goals
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctor₁₂Desc (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃)
    (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
    ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor₁₂Desc f =
      f i₁ i₂ i₃ h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{u_17, u_1} C₁
inst✝¹⁹ : Category.{u_16, u_2} C₂
inst✝¹⁸ : Category.{u_14, u_5} C₃
inst✝¹⁷ : Category.{u_13, u_6} C₄
inst✝¹⁶ : Category.{u_15, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
j : ι₄
A : C₄
f :
  (i₁ : ι₁) →
    (i₂ : ι₂) →
      (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A)
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor₁₂Desc f = f i₁ i₂ i₃ h

Tactic:
apply GradedObject.ι_mapBifunctor₁₂BifunctorDesc

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
lemma eventually_exists_mem_iff {is : Set β} {P : β → α → Prop} (his : is.Finite) :
    (∀ᶠ i in f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ i in f, P a i

Proof state:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x | P a x} ∈ f

Tactic:
convert f.finite_biUnion_mem_iff his (s := P) with i

Result:
case h.e'_1.h.e'_5
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} = ⋃ i ∈ is, P i

Proof state:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ (∀ᶠ (i : α) in ↑f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in ↑f, P a i

Tactic:
simp only [Filter.Eventually, Ultrafilter.mem_coe]

Result:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x | P a x} ∈ f

Proof state:
case h.e'_1.h.e'_5
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} = ⋃ i ∈ is, P i

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Ico : (fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)] (i : Fin m)
    (j : Fin (n i)) :
    (finPiFinEquiv (Pi.single i j : ∀ i : Fin m, Fin (n i)) : ℕ) =
      j * ∏ j, n (Fin.castLE i.is_lt.le j)

Proof state:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE ⋯ j) = 0

Tactic:
rintro x hx

Result:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE ⋯ j) = 0

Proof state:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE ⋯ j) = 0

Tactic:
rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

Result:
no goals

Proof state:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j : Fin ↑i, n (Fin.castLE ⋯ j)

Tactic:
rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]

Result:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE ⋯ j) = 0
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma inv_smul_lt_iff_of_neg (h : a < 0) : a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
a : α
b₁ b₂ : β
inst✝ : PosSMulStrictMono α β
h : a < 0
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

Tactic:
rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma decreasingInduction_succ_left  {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self)
    (smn : m + 1 ≤ n) (mn : m ≤ n) :
    decreasingInduction (motive := motive) of_succ self mn =
      of_succ m smn (decreasingInduction of_succ self smn)

Proof state:
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

Tactic:
rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn), decreasingInduction_trans,
  decreasingInduction_succ']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toArray_range' (start size step : Nat) :
    (range' start size step).toArray = Array.range' start size step

Proof state:
case h
start size step : Nat
⊢ (range' start size step).toArray.toList = (Array.range' start size step).toList

Tactic:
simp

Result:
no goals

Proof state:
start size step : Nat
⊢ (range' start size step).toArray = Array.range' start size step

Tactic:
apply ext'

Result:
case h
start size step : Nat
⊢ (range' start size step).toArray.toList = (Array.range' start size step).toList
-- Mathlib/Analysis/Quaternion.lean
theorem summable_coe {f : α → ℝ} : (Summable fun a => (f a : ℍ)) ↔ Summable f

Proof state:
α : Type u_1
f : α → ℝ
⊢ (Summable fun a => ↑(f a)) ↔ Summable f

Tactic:
simpa only using
  Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from
    QuaternionAlgebra.reₗ _ _ _)
    (continuous_algebraMap _ _) continuous_re coe_re

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma strictMono_rpow_of_base_gt_one {b : ℝ} (hb : 1 < b) :
    StrictMono (b ^ · : ℝ → ℝ)

Proof state:
b : ℝ
hb : 1 < b
⊢ StrictMono fun x => rexp (log b * x)

Tactic:
exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ StrictMono fun x => b ^ x

Tactic:
simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]

Result:
b : ℝ
hb : 1 < b
⊢ StrictMono fun x => rexp (log b * x)
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem Basis.ofZLatticeComap_apply (e : F ≃ₗ[K] E) {ι : Type*}
    (b : Basis ι ℤ L) (i : ι) :
    b.ofZLatticeComap K L e i = e.symm (b i)

Proof state:
K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
i : ι
⊢ ↑((ofZLatticeComap K L e b) i) = e.symm ↑(b i)

Tactic:
simp [Basis.ofZLatticeComap]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_zero_iff_of_ge {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s)
    {a b : α} (ha : a ∈ s) (hb : b ∈ s) (ba : b ≤ a) :
    variationOnFromTo f s a b = 0 ↔
      ∀ ⦃x⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0

Tactic:
rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
  or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Floor/Div.lean
lemma support_ceilDiv_subset : (f ⌈/⌉ a).support ⊆ f.support

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f : ι →₀ β
a : α
⊢ (f ⌈/⌉ a).support ⊆ f.support

Tactic:
simp +contextual [Finset.subset_iff, not_imp_not]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_ne_zero {e : ℕ} (he : e ≠ 0) (hle : map f p ≤ P ^ e)
    (hnle : ¬map f p ≤ P ^ (e + 1)) : ramificationIdx f p P ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
e : ℕ
he : e ≠ 0
hle : map f p ≤ P ^ e
hnle : ¬map f p ≤ P ^ (e + 1)
⊢ ramificationIdx f p P ≠ 0

Tactic:
rwa [ramificationIdx_spec hle hnle]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem add_one_le_of_lt (h : x < y) : x + 1 ≤ y

Proof state:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ succ x ≤ y

Tactic:
exact succ_le_of_lt h

Result:
no goals

Proof state:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ x + 1 ≤ y

Tactic:
rw [← succ_eq_add_one]

Result:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ succ x ≤ y
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem he'' (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g)
    {X' X Y} (f g) : F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ (e X Y) ((e X Y).symm g) = f ≫ g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)

Tactic:
rw [Equiv.eq_symm_apply, he]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ (e X Y) ((e X Y).symm g) = f ≫ g
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_to_nat : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℕ) < n) (m = n) ((n : ℕ) < m) : Prop)
  | 0, 0 => rfl
  | 0, pos _ => to_nat_pos _
  | pos _, 0 => to_nat_pos _
  | pos a, pos b => by
    have := PosNum.cmp_to_nat a b; revert this; dsimp [cmp]; cases PosNum.cmp a b
    exacts [id, congr_arg pos, id]

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (a.cmp b) → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (a.cmp b)

Proof state:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
revert this

Result:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Proof state:
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (a.cmp b) → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (a.cmp b)

Tactic:
cases PosNum.cmp a b

Result:
case lt
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.lt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.eq → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.gt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.gt

Proof state:
case lt
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.lt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.eq → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.gt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.gt

Tactic:
exacts [id, congr_arg pos, id]

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
have := PosNum.cmp_to_nat a b

Result:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_iff_of_neg' (hc : c < 0) : b / c ≤ a ↔ c * a ≤ b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
⊢ b / c ≤ a ↔ c * a ≤ b

Tactic:
rw [mul_comm, div_le_iff_of_neg hc]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_le_ker_coord_iff [Nontrivial R] (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} :
    b.flag k ≤ LinearMap.ker (b.coord l) ↔ k ≤ l.castSucc

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
n : ℕ
inst✝ : Nontrivial R
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
⊢ b.flag k ≤ LinearMap.ker (b.coord l) ↔ k ≤ l.castSucc

Tactic:
simp [flag_le_iff, Finsupp.single_apply_eq_zero, imp_false, imp_not_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem disjoint_list_sum_right {a : Multiset α} {l : List (Multiset α)} :
    Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

Proof state:
α : Type u_3
a : Multiset α
l : List (Multiset α)
⊢ Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

Tactic:
simpa only [disjoint_comm (a := a)] using disjoint_list_sum_left

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem pow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℕ, (f ^ n) x = x
  | 0 => rfl
  | n + 1 => by rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]

Proof state:
α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ (n + 1)) x = x

Tactic:
rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_card (a : K) : a ^ q = a

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q = a

Tactic:
by_cases h : a = 0

Result:
case pos
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : a = 0
⊢ a ^ q = a

case neg
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : ¬a = 0
⊢ a ^ q = a

Proof state:
case pos
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : a = 0
⊢ 0 ^ q = 0

Tactic:
apply zero_pow Fintype.card_ne_zero

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : a = 0
⊢ a ^ q = a

Tactic:
rw [h]

Result:
case pos
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : a = 0
⊢ 0 ^ q = 0

Proof state:
case neg
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : ¬a = 0
⊢ a ^ q = a

Tactic:
rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one,
  pow_card_sub_one_eq_one a h, one_mul]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem restrict_preimage_emb {f : α → β} (hf : MeasurePreserving f μa μb)
    (h₂ : MeasurableEmbedding f) (s : Set β) :
    MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) :=
  ⟨hf.measurable, by rw [← hf.map_eq, h₂.restrict_map]⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
rw [← hf.map_eq, h₂.restrict_map]

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem toEnd_restrict_eq_toEnd (h := N.toEnd_comp_subtype_mem x) :
    (toEnd R L M x).restrict h = toEnd R L N x

Proof state:
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯
x✝ : ↥↑N
⊢ ↑((LinearMap.restrict ((toEnd R L M) x) h) x✝) = ↑(((toEnd R L ↥N) x) x✝)

Tactic:
simp only [LinearMap.restrict_coe_apply, toEnd_apply_apply, ← coe_bracket,
  SetLike.coe_eq_coe]

Result:
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯
x✝ : ↥↑N
⊢ ⁅x, x✝⁆ = ((toEnd R L ↥N) x) x✝

Proof state:
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯
x✝ : ↥↑N
⊢ ⁅x, x✝⁆ = ((toEnd R L ↥N) x) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯
⊢ LinearMap.restrict ((toEnd R L M) x) h = (toEnd R L ↥N) x

Tactic:
ext

Result:
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯
x✝ : ↥↑N
⊢ ↑((LinearMap.restrict ((toEnd R L M) x) h) x✝) = ↑(((toEnd R L ↥N) x) x✝)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem _root_.Set.Infinite.meas_eq_top [MeasurableSingletonClass α]
    {s : Set α} (hs : s.Infinite) (h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}) : μ s = ∞ := top_unique <|
  let ⟨ε, hne, hε⟩ := h'; have := hs.to_subtype
  calc
    ∞ = ∑' _ : s, ε := (ENNReal.tsum_const_eq_top_of_ne_zero hne).symm
    _ ≤ ∑' x : s, μ {x.1} := ENNReal.tsum_le_tsum fun x ↦ hε x x.2
    _ ≤ μ (⋃ x : s, {x.1}) := tsum_meas_le_meas_iUnion_of_disjoint _
      (fun _ ↦ MeasurableSet.singleton _) fun x y hne ↦ by simpa [Subtype.val_inj]
    _ = μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Infinite
h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}
ε : ℝ≥0∞
hne : ε ≠ 0
hε : ∀ x ∈ s, ε ≤ μ {x}
this : Infinite ↑s
⊢ μ (⋃ x, {↑x}) = μ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Infinite
h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}
ε : ℝ≥0∞
hne✝ : ε ≠ 0
hε : ∀ x ∈ s, ε ≤ μ {x}
this : Infinite ↑s
x y : ↑s
hne : x ≠ y
⊢ (Disjoint on fun x => {↑x}) x y

Tactic:
simpa [Subtype.val_inj]

Result:
no goals