harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean
theorem effectiveEpiFamilyStructOfEffectiveEpiDesc_aux {B : C} {α : Type*} {X : α → C}
    {π : (a : α) → X a ⟶ B} [HasCoproduct X]
    [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)]
    [∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)]
    [∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))]
    {W : C} {e : (a : α) → X a ⟶ W} (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) {Z : C}
    {g₁ g₂ : Z ⟶ ∐ fun b ↦ X b} (hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π) :
    g₁ ≫ Sigma.desc e = g₂ ≫ Sigma.desc e

Proof state:
case h.h.a
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b => X b
a b : α
hg :
  Sigma.ι (fun a_1 => pullback (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) b ≫
      (Sigma.desc fun a_1 => pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) ≫
        pullback.snd g₁ (Sigma.ι X a) ≫ π a =
    Sigma.ι (fun a_1 => pullback (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) b ≫
      (Sigma.desc fun a_1 => pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) ≫
        pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b

Tactic:
simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app] at hg

Result:
case h.h.a
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b => X b
a b : α
hg :
  pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ π a =
    pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarContent_outerMeasure_self_pos (K₀ : PositiveCompacts G) :
    0 < (haarContent K₀).outerMeasure K₀

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : IsOpen U
hK₀ : ↑K₀ ⊆ U
⊢ 1 ≤ (haarContent K₀) K₀.toCompacts

Tactic:
exact haarContent_self.ge

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ 1 ≤ (haarContent K₀).outerMeasure ↑K₀

Tactic:
rw [Content.outerMeasure_eq_iInf]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ 1 ≤ ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : ↑K₀ ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU }

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ 0 < (haarContent K₀).outerMeasure ↑K₀

Tactic:
refine zero_lt_one.trans_le ?_

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ 1 ≤ (haarContent K₀).outerMeasure ↑K₀

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ 1 ≤ ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : ↑K₀ ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU }

Tactic:
refine le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans ?_ <| le_iSup₂ K₀.toCompacts hK₀

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : IsOpen U
hK₀ : ↑K₀ ⊆ U
⊢ 1 ≤ (haarContent K₀) K₀.toCompacts
-- Mathlib/GroupTheory/Perm/Support.lean
theorem mem_support_swap_mul_imp_mem_support_ne {x y : α} (hy : y ∈ support (swap x (f x) * f)) :
    y ∈ support f ∧ y ≠ x

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : f y = x
⊢ f y ≠ y ∧ y ≠ x

Tactic:
constructor <;> intro <;> simp_all only [if_true, eq_self_iff_true, not_true, Ne]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
y : α
h : ¬f y = y
hy : y ≠ y
⊢ f y ≠ y ∧ y ≠ y

Tactic:
exact ⟨h, hy⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (swap x (f x) * f).support
⊢ y ∈ f.support ∧ y ≠ x

Tactic:
simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
⊢ f y ≠ y ∧ y ≠ x

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : ¬f y = x
⊢ f y ≠ y ∧ y ≠ x

Tactic:
split_ifs at hy with heq

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h : ¬f y = x
heq : y = x
hy : x ≠ y
⊢ f y ≠ y ∧ y ≠ x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h : ¬f y = x
heq : ¬y = x
hy : f y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h : ¬f y = x
heq : y = x
hy : x ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
subst heq

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
y : α
h : ¬f y = y
hy : y ≠ y
⊢ f y ≠ y ∧ y ≠ y

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h : ¬f y = x
heq : ¬y = x
hy : f y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
exact ⟨hy, heq⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
by_cases h : f y = x

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : f y = x
⊢ f y ≠ y ∧ y ≠ x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : ¬f y = x
⊢ f y ≠ y ∧ y ≠ x
-- Mathlib/Data/Finset/Sort.lean
theorem _root_.List.toFinset_sort [DecidableEq α] {l : List α} (hl : l.Nodup) :
    sort r l.toFinset = l ↔ l.Sorted r

Proof state:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
h : sort r l.toFinset = l
⊢ List.Sorted r l

Tactic:
rw [← h]

Result:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
h : sort r l.toFinset = l
⊢ List.Sorted r (sort r l.toFinset)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ sort r l.toFinset = l → List.Sorted r l

Tactic:
intro h

Result:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
h : sort r l.toFinset = l
⊢ List.Sorted r l

Proof state:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ sort r l.toFinset = l ↔ List.Sorted r l

Tactic:
refine ⟨?_, List.eq_of_perm_of_sorted ((sort_perm_toList r _).trans (List.toFinset_toList hl))
  (sort_sorted r _)⟩

Result:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ sort r l.toFinset = l → List.Sorted r l

Proof state:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
h : sort r l.toFinset = l
⊢ List.Sorted r (sort r l.toFinset)

Tactic:
exact sort_sorted r _

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma mulOption_lt_mul_of_equiv (hn : x₁.Numeric) (h : IH24 x₁ x₂ y) (he : x₁ ≈ x₂) (i j) :
    ⟦mulOption x₁ y i j⟧ < (⟦x₂ * y⟧ : Game)

Proof state:
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ ⟦x₁.mulOption y i j⟧ < ⟦x₂ * y⟧

Tactic:
convert sub_lt_iff_lt_add'.2 ((((@h _).1 <| IsOption.moveLeft i).2 _).1 j) using 1

Result:
case h.e'_3
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ ⟦x₁.mulOption y i j⟧ = ⟦x₁.moveLeft i * y⟧ + ⟦x₂ * y.moveLeft j⟧ - ⟦x₁.moveLeft i * y.moveLeft j⟧

x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ x₁.moveLeft i < x₂

Proof state:
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ x₁.moveLeft i < x₂

Tactic:
rw [← lt_congr_right he]

Result:
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ x₁.moveLeft i < x₁

Proof state:
case h.e'_3
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ ⟦x₁.mulOption y i j⟧ = ⟦x₁.moveLeft i * y⟧ + ⟦x₁ * y.moveLeft j⟧ - ⟦x₁.moveLeft i * y.moveLeft j⟧

Tactic:
rfl

Result:
no goals

Proof state:
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ x₁.moveLeft i < x₁

Tactic:
apply hn.moveLeft_lt

Result:
no goals

Proof state:
case h.e'_3
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ ⟦x₁.mulOption y i j⟧ = ⟦x₁.moveLeft i * y⟧ + ⟦x₂ * y.moveLeft j⟧ - ⟦x₁.moveLeft i * y.moveLeft j⟧

Tactic:
rw [← ((@h _).2.2 <| IsOption.moveLeft j).1 he]

Result:
case h.e'_3
x₁ x₂ y : PGame
hn : x₁.Numeric
h : IH24 x₁ x₂ y
he : x₁ ≈ x₂
i : x₁.LeftMoves
j : y.LeftMoves
⊢ ⟦x₁.mulOption y i j⟧ = ⟦x₁.moveLeft i * y⟧ + ⟦x₁ * y.moveLeft j⟧ - ⟦x₁.moveLeft i * y.moveLeft j⟧
-- Mathlib/Data/Rat/Defs.lean
lemma pow_eq_mkRat (q : ℚ) (n : ℕ) : q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Proof state:
q : ℚ
n : ℕ
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Tactic:
rw [pow_def, mk_eq_mkRat]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem classified : h.IsClassified

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ⋯.IsPrimitiveClassified

Tactic:
apply h.normalize.isPrimitiveClassified_of_coprime

Result:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ (x / ↑(x.gcd y)).gcd (y / ↑(x.gcd y)) = 1

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ (x / ↑(x.gcd y)).gcd (y / ↑(x.gcd y)) = 1

Tactic:
apply Int.gcd_div_gcd_div_gcd (Nat.pos_of_ne_zero h0)

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x.natAbs = 0

Tactic:
apply Nat.eq_zero_of_gcd_eq_zero_left h0

Result:
no goals

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ h.IsClassified

Tactic:
use 0, 1, 0

Result:
case h
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ (x = 0 * (1 ^ 2 - 0 ^ 2) ∧ y = 0 * (2 * 1 * 0) ∨ x = 0 * (2 * 1 * 0) ∧ y = 0 * (1 ^ 2 - 0 ^ 2)) ∧ Int.gcd 1 0 = 1

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ h.IsClassified

Tactic:
apply h.isClassified_of_normalize_isPrimitiveClassified

Result:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ⋯.IsPrimitiveClassified

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ h.IsClassified

Tactic:
have hy : y = 0 := by
  apply Int.natAbs_eq_zero.mp
  apply Nat.eq_zero_of_gcd_eq_zero_right h0

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ h.IsClassified

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified

Tactic:
have hx : x = 0 := by
  apply Int.natAbs_eq_zero.mp
  apply Nat.eq_zero_of_gcd_eq_zero_left h0

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ h.IsClassified

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x = 0

Tactic:
apply Int.natAbs_eq_zero.mp

Result:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x.natAbs = 0

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y.natAbs = 0

Tactic:
apply Nat.eq_zero_of_gcd_eq_zero_right h0

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ h.IsClassified

Tactic:
by_cases h0 : Int.gcd x y = 0

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ h.IsClassified

Proof state:
case h
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ (x = 0 * (1 ^ 2 - 0 ^ 2) ∧ y = 0 * (2 * 1 * 0) ∨ x = 0 * (2 * 1 * 0) ∧ y = 0 * (1 ^ 2 - 0 ^ 2)) ∧ Int.gcd 1 0 = 1

Tactic:
field_simp [hx, hy]

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y = 0

Tactic:
apply Int.natAbs_eq_zero.mp

Result:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y.natAbs = 0
-- Mathlib/Data/Int/Cast/Field.lean
theorem cast_neg_natCast {R} [DivisionRing R] (n : ℕ) : ((-n : ℤ) : R) = -n

Proof state:
R : Type u_2
inst✝ : DivisionRing R
n : ℕ
⊢ ↑(-↑n) = -↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem stream_succ_of_int (a : ℤ) (n : ℕ) : IntFractPair.stream (a : K) (n + 1) = none

Proof state:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
⊢ (IntFractPair.of ↑a).fr = 0

Tactic:
simp only [IntFractPair.of, Int.fract_intCast]

Result:
no goals

Proof state:
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
n : ℕ
ih : IntFractPair.stream (↑a) (n + 1) = none
⊢ IntFractPair.stream (↑a) (n + 1 + 1) = none

Tactic:
exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
n : ℕ
⊢ IntFractPair.stream (↑a) (n + 1) = none

Tactic:
induction n with
| zero =>
  refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_
  simp only [IntFractPair.of, Int.fract_intCast]
| succ n ih => exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

Result:
no goals

Proof state:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
⊢ IntFractPair.stream (↑a) (0 + 1) = none

Tactic:
refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_

Result:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : ℤ
⊢ (IntFractPair.of ↑a).fr = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
    l.contains a ↔ a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ l.contains a = true ↔ a ∈ l

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem disjoint_comap (h : Disjoint g₁ g₂) : Disjoint (comap m g₁) (comap m g₂)

Proof state:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Disjoint g₁ g₂
⊢ Disjoint (comap m g₁) (comap m g₂)

Tactic:
simp only [disjoint_iff, ← comap_inf, h.eq_bot, comap_bot]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_of_lt_order {d : σ →₀ ℕ} (h : degree d < f.order) :
    coeff R d f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑d.degree < f.order
⊢ (coeff R d) f = 0

Tactic:
rw [degree_eq_weight_one] at h

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x => 1) d) < f.order
⊢ (coeff R d) f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x => 1) d) < f.order
⊢ (coeff R d) f = 0

Tactic:
exact coeff_eq_zero_of_lt_weightedOrder _ h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_flatten (L : Array (Array α)) :
    L.flatten.reverse = (L.map reverse).reverse.flatten

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten.reverse =
    (map reverse (List.map List.toArray xss✝).toArray).reverse.flatten

Tactic:
simp [flatten_toArray, List.reverse_flatten, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.flatten.reverse = (map reverse L).reverse.flatten

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten.reverse =
    (map reverse (List.map List.toArray xss✝).toArray).reverse.flatten
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma one_half_lt_eulerMascheroniSeq_six : 1 / 2 < eulerMascheroniSeq 6

Proof state:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < ∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / ↑i.factorial

Tactic:
simp_rw [Finset.sum_range_succ, Nat.factorial_succ]

Result:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 <
    ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / ↑i.factorial + (49 / 20 - 1 / 2) ^ 0 / ↑(Nat.factorial 0) +
                (49 / 20 - 1 / 2) ^ 1 / ↑((0 + 1) * Nat.factorial 0) +
              (49 / 20 - 1 / 2) ^ 2 / ↑((1 + 1) * ((0 + 1) * Nat.factorial 0)) +
            (49 / 20 - 1 / 2) ^ 3 / ↑((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))) +
          (49 / 20 - 1 / 2) ^ 4 / ↑((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0)))) +
        (49 / 20 - 1 / 2) ^ 5 / ↑((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))) +
      (49 / 20 - 1 / 2) ^ 6 / ↑((5 + 1) * ((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))))

Proof state:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 0 < 7

Tactic:
positivity

Result:
no goals

Proof state:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 <
    ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / ↑i.factorial + (49 / 20 - 1 / 2) ^ 0 / ↑(Nat.factorial 0) +
                (49 / 20 - 1 / 2) ^ 1 / ↑((0 + 1) * Nat.factorial 0) +
              (49 / 20 - 1 / 2) ^ 2 / ↑((1 + 1) * ((0 + 1) * Nat.factorial 0)) +
            (49 / 20 - 1 / 2) ^ 3 / ↑((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))) +
          (49 / 20 - 1 / 2) ^ 4 / ↑((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0)))) +
        (49 / 20 - 1 / 2) ^ 5 / ↑((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))) +
      (49 / 20 - 1 / 2) ^ 6 / ↑((5 + 1) * ((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))))

Tactic:
norm_num

Result:
no goals

Proof state:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
rw [this, lt_sub_iff_add_lt, ← lt_sub_iff_add_lt', log_lt_iff_lt_exp (by positivity)]

Result:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < rexp (49 / 20 - 1 / 2)

Proof state:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 0 ≤ 49 / 20 - 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ ↑(harmonic 6) - log (↑6 + 1) = 49 / 20 - log 7

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
have : eulerMascheroniSeq 6 = 49 / 20 - log 7 := by
  rw [eulerMascheroniSeq]
  norm_num

Result:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 < eulerMascheroniSeq 6

Proof state:
⊢ eulerMascheroniSeq 6 = 49 / 20 - log 7

Tactic:
rw [eulerMascheroniSeq]

Result:
⊢ ↑(harmonic 6) - log (↑6 + 1) = 49 / 20 - log 7

Proof state:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < rexp (49 / 20 - 1 / 2)

Tactic:
refine lt_of_lt_of_le ?_ (Real.sum_le_exp_of_nonneg (by norm_num) 7)

Result:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < ∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / ↑i.factorial
-- Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean
theorem IsExtrFilter.lineDeriv_eq_zero {l : Filter E} (h : IsExtrFilter f l a)
    (h' : Tendsto (fun t : ℝ ↦ a + t • b) (𝓝 0) l) : lineDeriv ℝ f a b = 0

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E → ℝ
a b : E
l : Filter E
h : IsExtrFilter f l a
h' : Tendsto (fun t => a + t • b) (𝓝 0) l
⊢ lineDeriv ℝ f a b = 0

Tactic:
classical
exact if hd : LineDifferentiableAt ℝ f a b then
  h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
else
  lineDeriv_zero_of_not_lineDifferentiableAt hd

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E → ℝ
a b : E
l : Filter E
h : IsExtrFilter f l a
h' : Tendsto (fun t => a + t • b) (𝓝 0) l
⊢ lineDeriv ℝ f a b = 0

Tactic:
exact if hd : LineDifferentiableAt ℝ f a b then
  h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
else
  lineDeriv_zero_of_not_lineDifferentiableAt hd

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
lemma support_monotone : Monotone (support (α := ι) (M := α)) :=
  fun f g h a ha ↦ by rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢; exact ha.trans_le (h _)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : a ∈ f.support
⊢ a ∈ g.support

Tactic:
rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢

Result:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a

Tactic:
exact ha.trans_le (h _)

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem pow (m : ℕ) (h : a ≡ b [ZMOD n]) : a ^ m ≡ b ^ m [ZMOD n]

Proof state:
case zero
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ 0 ≡ b ^ 0 [ZMOD n]

Tactic:
rfl

Result:
no goals

Proof state:
case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ d * a ≡ b ^ d * b [ZMOD n]

Tactic:
exact hd.mul h

Result:
no goals

Proof state:
n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]

Tactic:
induction' m with d hd

Result:
case zero
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ 0 ≡ b ^ 0 [ZMOD n]

case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [ZMOD n]

Proof state:
case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [ZMOD n]

Tactic:
rw [pow_succ, pow_succ]

Result:
case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ d * a ≡ b ^ d * b [ZMOD n]