harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Fermat.lean
theorem Int.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) :
    (fermatNumber (n + 2) : ℤ)  = (fermatNumber (n + 1)) ^ 2 - 2 * (fermatNumber n - 1) ^ 2

Proof state:
n : ℕ
⊢ ↑(n + 2).fermatNumber = ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2

Tactic:
rw [Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq,
  Nat.cast_sub <| two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq n]

Result:
n : ℕ
⊢ ↑((n + 1).fermatNumber ^ 2) - ↑(2 * (n.fermatNumber - 1) ^ 2) =
    ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2

Proof state:
n : ℕ
⊢ ↑((n + 1).fermatNumber ^ 2) - ↑(2 * (n.fermatNumber - 1) ^ 2) =
    ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2

Tactic:
simp only [fermatNumber, push_cast, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem add_product (s t : Multiset α) (u : Multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

Proof state:
α : Type u_1
β : Type v
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

Tactic:
simp [SProd.sprod, product]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_add_mkRat (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * d₂ + n₂ * d₁) (d₁ * d₂)

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂)

Tactic:
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_add_normalize, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.Tendsto.prodMap_nhds {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W}
    (hf : Tendsto f (𝓝 x) (𝓝 y)) (hg : Tendsto g (𝓝 z) (𝓝 w)) :
    Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w))

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w))

Tactic:
rw [nhds_prod_eq, nhds_prod_eq]

Result:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)

Tactic:
exact hf.prod_map hg

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_psigma {α} {E : α → Sort*} : IsEmpty (PSigma E) ↔ ∀ a, IsEmpty (E a)

Proof state:
α : Sort u_5
E : α → Sort u_4
⊢ IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)

Tactic:
simp only [← not_nonempty_iff, nonempty_psigma, not_exists]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndepSets.meas_iInter [Fintype ι] (h : iIndepSets π κ μ) (hs : ∀ i, s i ∈ π i) :
    ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)

Tactic:
filter_upwards [h.meas_biInter Finset.univ (fun _i _ ↦ hs _)] with a ha using by simp [← ha]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
a : α
ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i : ι, (κ a) (s i)
⊢ (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)

Tactic:
simp [← ha]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
lemma exists_lt_mem_inter_of_not_pairwiseDisjoint [LinearOrder ι]
    {f : ι → Set α} (h : ¬ s.PairwiseDisjoint f) :
    ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt

Result:
case intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

case intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem sup {f g : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) (hg : Submartingale g ℱ μ) :
    Submartingale (f ⊔ g) ℱ μ

Proof state:
case refine_1
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]

Tactic:
exact EventuallyLE.trans (hf.2.1 i j hij)
  (condExp_mono (hf.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
    (Eventually.of_forall fun x => le_max_left _ _))

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Submartingale (f ⊔ g) ℱ μ

Tactic:
refine ⟨fun i => @StronglyMeasurable.sup _ _ _ _ (ℱ i) _ _ _ (hf.adapted i) (hg.adapted i),
  fun i j hij => ?_, fun i => Integrable.sup (hf.integrable _) (hg.integrable _)⟩

Result:
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ (f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]

Tactic:
refine EventuallyLE.sup_le ?_ ?_

Result:
case refine_1
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]

case refine_2
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ g i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]

Proof state:
case refine_2
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f g : ι → Ω → ℝ
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ g i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]

Tactic:
exact EventuallyLE.trans (hg.2.1 i j hij)
  (condExp_mono (hg.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
    (Eventually.of_forall fun x => le_max_right _ _))

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem toList_append (l₁ l₂ : DList α) : toList (l₁ ++ l₂) = toList l₁ ++ toList l₂

Proof state:
α : Type u_1
l₁ l₂ : DList α
⊢ l₁.apply (l₂.apply []) = l₁.apply [] ++ l₂.apply []

Tactic:
rw [invariant]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : DList α
⊢ (l₁ ++ l₂).toList = l₁.toList ++ l₂.toList

Tactic:
simp only [toList, append, Function.comp]

Result:
α : Type u_1
l₁ l₂ : DList α
⊢ l₁.apply (l₂.apply []) = l₁.apply [] ++ l₂.apply []
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma extendHomologyIso_hom_naturality :
    homologyMap (extendMap φ e) j' ≫ (L.extendHomologyIso e hj').hom =
      (K.extendHomologyIso e hj').hom ≫ homologyMap φ j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{u_4, u_3} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ homologyMap (extendMap φ e) j' ≫ (L.extendHomologyIso e hj').hom = (K.extendHomologyIso e hj').hom ≫ homologyMap φ j

Tactic:
simp [← cancel_epi ((K.extend e).homologyπ _)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_nil : l <+~ [] ↔ l = [] :=
  ⟨fun h => length_eq_zero.1 $ Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩

Proof state:
α✝ : Type u_1
l : List α✝
⊢ l = [] → l <+~ []

Tactic:
rintro rfl

Result:
α✝ : Type u_1
⊢ [] <+~ []

Proof state:
α✝ : Type u_1
⊢ [] <+~ []

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_leftUnshift {a n' : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn' : n + a = n') :
    (γ.leftUnshift n hn').leftShift a n' hn' = γ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
⊢ (γ.leftUnshift n hn').leftShift a n' hn' = γ

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq

Tactic:
rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q-n) (by omega),
  γ.leftUnshift_v n hn' (q-n) q (by omega) p hpq, Linear.comp_units_smul, smul_smul,
  Iso.hom_inv_id_assoc, Int.units_mul_self, one_smul]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ q - n + n = q

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_norm_eq_idemFst_sup_idemSnd (x : WithLp ∞ (α × β)) :
    ‖x‖ = max ‖idemFst x‖ ‖idemSnd x‖

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp ⊤ (α × β)
⊢ ‖x‖ = ‖idemFst x‖ ⊔ ‖idemSnd x‖

Tactic:
rw [WithLp.prod_norm_eq_sup, ← WithLp.norm_equiv_symm_fst ∞ α β x.1,
  ← WithLp.norm_equiv_symm_snd ∞ α β x.2]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp ⊤ (α × β)
⊢ ‖(WithLp.equiv ⊤ (α × β)).symm (x.1, 0)‖ ⊔ ‖(WithLp.equiv ⊤ (α × β)).symm (0, x.2)‖ = ‖idemFst x‖ ⊔ ‖idemSnd x‖

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp ⊤ (α × β)
⊢ ‖(WithLp.equiv ⊤ (α × β)).symm (x.1, 0)‖ ⊔ ‖(WithLp.equiv ⊤ (α × β)).symm (0, x.2)‖ = ‖idemFst x‖ ⊔ ‖idemSnd x‖

Tactic:
rfl

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean
theorem structuralIsoOfExpr_horizontalComp {f₁ g₁ f₂ g₂ : C}
    (η : f₁ ⟶ g₁) (η' : f₁ ≅ g₁) (ih_η : η'.hom = η)
    (θ : f₂ ⟶ g₂) (θ' : f₂ ≅ g₂) (ih_θ : θ'.hom = θ) :
    (η' ⊗ θ').hom = η ⊗ θ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f₁ g₁ f₂ g₂ : C
η : f₁ ⟶ g₁
η' : f₁ ≅ g₁
ih_η : η'.hom = η
θ : f₂ ⟶ g₂
θ' : f₂ ≅ g₂
ih_θ : θ'.hom = θ
⊢ (η' ⊗ θ').hom = η ⊗ θ

Tactic:
simp [ih_η, ih_θ]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_eq_union : [[a, b]] = Icc a b ∪ Icc b a :=
  coe_injective <| by
    push_cast
    exact Set.uIcc_eq_union

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a

Tactic:
exact Set.uIcc_eq_union

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ ↑[[a, b]] = ↑(Icc a b ∪ Icc b a)

Tactic:
push_cast

Result:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.WF.merge_node (h₁ : NodeWF le a₁ c₁) (h₂ : NodeWF le a₂ c₂) :
    (merge le (.node a₁ c₁ s₁) (.node a₂ c₂ s₂)).WF le

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le (merge le (Heap.node a₁ c₁ s₁) (Heap.node a₂ c₂ s₂))

Tactic:
unfold merge

Result:
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (match Heap.node a₁ c₁ s₁, Heap.node a₂ c₂ s₂ with
    | Heap.nil, Heap.nil => Heap.nil
    | Heap.nil, Heap.node a₂ c₂ sibling => Heap.node a₂ c₂ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.nil => Heap.node a₁ c₁ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil
      else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)

Tactic:
split <;> rename_i h

Result:
case isTrue
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : le a₁ a₂ = true
⊢ WF le (Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil)

case isFalse
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : ¬le a₁ a₂ = true
⊢ WF le (Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)

Proof state:
case isFalse
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : ¬le a₁ a₂ = true
⊢ WF le (Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)

Tactic:
exact node ⟨fun [_] => TotalBLE.total.resolve_left h, h₁, h₂⟩

Result:
no goals

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (match Heap.node a₁ c₁ s₁, Heap.node a₂ c₂ s₂ with
    | Heap.nil, Heap.nil => Heap.nil
    | Heap.nil, Heap.node a₂ c₂ sibling => Heap.node a₂ c₂ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.nil => Heap.node a₁ c₁ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil
      else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)

Tactic:
dsimp

Result:
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)

Proof state:
case isTrue
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : le a₁ a₂ = true
⊢ WF le (Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil)

Tactic:
exact node ⟨fun [_] => h, h₂, h₁⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma hilbertPoly_X_pow_succ (d k : ℕ) :
    hilbertPoly ((X : F[X]) ^ k) (d + 1) = preHilbertPoly F d k

Proof state:
F : Type u_1
inst✝ : Field F
d k : ℕ
⊢ (X ^ k).hilbertPoly (d + 1) = preHilbertPoly F d k

Tactic:
delta hilbertPoly

Result:
F : Type u_1
inst✝ : Field F
d k : ℕ
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (X ^ k).support, (X ^ k).coeff i • preHilbertPoly F d i) =
    preHilbertPoly F d k

Proof state:
F : Type u_1
inst✝ : Field F
d k : ℕ
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (X ^ k).support, (X ^ k).coeff i • preHilbertPoly F d i) =
    preHilbertPoly F d k

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂'_conj (z τ : ℂ) :
    conj (jacobiTheta₂' z τ) = jacobiTheta₂' (conj z) (-conj τ)

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ -(starRingEnd ℂ) (jacobiTheta₂'_term n z τ) = jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, map_mul, ← Complex.exp_conj, map_add, map_mul,
  ← ofReal_intCast,← ofReal_ofNat, map_pow, conj_ofReal, conj_I]

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ -(↑2 * ↑π * -I * ↑↑n * cexp (↑2 * ↑π * -I * ↑↑n * (starRingEnd ℂ) z + ↑π * -I * ↑↑n ^ 2 * (starRingEnd ℂ) τ)) =
    ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ -(↑2 * ↑π * -I * ↑↑n * cexp (↑2 * ↑π * -I * ↑↑n * (starRingEnd ℂ) z + ↑π * -I * ↑↑n ^ 2 * (starRingEnd ℂ) τ)) =
    ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)

Tactic:
ring_nf

Result:
no goals

Proof state:
z τ : ℂ
⊢ ∑' (b : ℤ), -(starRingEnd ℂ) (jacobiTheta₂'_term b z τ) =
    ∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
congr 1 with n

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ -(starRingEnd ℂ) (jacobiTheta₂'_term n z τ) = jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Proof state:
z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
rw [← neg_inj, ← jacobiTheta₂'_neg_left, jacobiTheta₂', jacobiTheta₂', conj_tsum, ← tsum_neg]

Result:
z τ : ℂ
⊢ ∑' (b : ℤ), -(starRingEnd ℂ) (jacobiTheta₂'_term b z τ) =
    ∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ Set.Ioc (-π) π) : arg (cos θ + sin θ * I) = θ

Proof state:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (cos ↑θ + sin ↑θ * I).arg = θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
lemma Complex.cot_pi_eq_exp_ratio (z : ℂ) :
    cot (π * z) = (Complex.exp (2 * π * I * z) + 1) / (I * (1 - Complex.exp (2 * π * I * z)))

Proof state:
z : ℂ
⊢ (cexp (2 * I * (↑π * z)) + 1) / (I * (1 - cexp (2 * I * (↑π * z)))) =
    (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))

Tactic:
ring_nf

Result:
no goals

Proof state:
z : ℂ
⊢ (↑π * z).cot = (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))

Tactic:
rw [cot_eq_exp_ratio (π * z)]

Result:
z : ℂ
⊢ (cexp (2 * I * (↑π * z)) + 1) / (I * (1 - cexp (2 * I * (↑π * z)))) =
    (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))
-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
theorem toLimit_injective (P : ProfiniteGrp.{u}) : Function.Injective (toLimit P)

Proof state:
case intro
P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
H : OpenNormalSubgroup ↑P.toProfinite.toTop
hH : ↑H ⊆ {x}ᶜ
⊢ False

Tactic:
exact hH ((QuotientGroup.eq_one_iff x).mp (congrFun (Subtype.val_inj.mpr h) H)) rfl

Result:
no goals

Proof state:
P : ProfiniteGrp.{u}
⊢ ∀ x ∈ (Hom.hom P.toLimit).ker, x = 1

Tactic:
intro x h

Result:
P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
⊢ x = 1

Proof state:
P : ProfiniteGrp.{u}
⊢ Function.Injective ⇑(Hom.hom P.toLimit).toMonoidHom

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, Subgroup.eq_bot_iff_forall]

Result:
P : ProfiniteGrp.{u}
⊢ ∀ x ∈ (Hom.hom P.toLimit).ker, x = 1

Proof state:
P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
⊢ False

Tactic:
rcases exist_openNormalSubgroup_sub_open_nhd_of_one (isOpen_compl_singleton)
  (Set.mem_compl_singleton_iff.mpr fun a => xne1 a.symm) with ⟨H, hH⟩

Result:
case intro
P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
H : OpenNormalSubgroup ↑P.toProfinite.toTop
hH : ↑H ⊆ {x}ᶜ
⊢ False

Proof state:
P : ProfiniteGrp.{u}
⊢ Function.Injective ⇑(Hom.hom P.toLimit)

Tactic:
show Function.Injective (toLimit P).hom.toMonoidHom

Result:
P : ProfiniteGrp.{u}
⊢ Function.Injective ⇑(Hom.hom P.toLimit).toMonoidHom

Proof state:
P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
⊢ x = 1

Tactic:
by_contra xne1

Result:
P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
⊢ False
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem left_le_lineMap_iff_le (h : 0 < r) : a ≤ lineMap a b r ↔ a ≤ b :=
  Iff.trans (by rw [lineMap_apply_zero]) (lineMap_le_lineMap_iff_of_lt h)

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r : k
h : 0 < r
⊢ a ≤ (lineMap a b) r ↔ (lineMap a b) 0 ≤ (lineMap a b) r

Tactic:
rw [lineMap_apply_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_self (c : Bool) (t : α) : cond c t t = t

Proof state:
α : Type u_1
c : Bool
t : α
⊢ (bif c then t else t) = t

Tactic:
cases c <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isClosed_comap_singleton_of_isIntegral (hf : f.IsIntegral)
    (x : PrimeSpectrum S) (hx : IsClosed ({x} : Set (PrimeSpectrum S))) :
    IsClosed ({comap f x} : Set (PrimeSpectrum R))

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
x : PrimeSpectrum S
hx : IsClosed {x}
⊢ IsClosed {(comap f) x}

Tactic:
simpa using isClosedMap_comap_of_isIntegral f hf _ hx

Result:
no goals