harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_insert_insert_insert_left_of_mem_affineSpan_pair {p₁ p₂ p₃ p₄ p₅ : P}
    (h₁ : p₁ ∈ line[k, p₄, p₅]) (h₂ : p₂ ∈ line[k, p₄, p₅]) (h₃ : p₃ ∈ line[k, p₄, p₅]) :
    Collinear k ({p₁, p₂, p₃, p₄} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃, p₄} ⊆ {p₁, p₂, p₃, p₄, p₅}

Tactic:
repeat apply Set.insert_subset_insert

Result:
case h.h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₄} ⊆ {p₄, p₅}

Proof state:
case h.h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₄} ⊆ {p₄, p₅}

Tactic:
simp

Result:
no goals

Proof state:
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₃, p₄} ⊆ {p₃, p₄, p₅}

Tactic:
apply Set.insert_subset_insert

Result:
case h.h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₄} ⊆ {p₄, p₅}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₁, p₂, p₃, p₄}

Tactic:
refine (collinear_insert_insert_insert_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃, p₄} ⊆ {p₁, p₂, p₃, p₄, p₅}
-- Mathlib/Topology/Category/Stonean/Limits.lean
lemma extremallyDisconnected_preimage : ExtremallyDisconnected (i ⁻¹' (Set.range f)) where
  open_closure U hU

Proof state:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
h : IsClopen (⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
⊢ IsOpen ((fun a => ↑a) ⁻¹' closure (Subtype.val '' U))

Tactic:
exact isOpen_induced (ExtremallyDisconnected.open_closure _
  (h.2.isOpenEmbedding_subtypeVal.isOpenMap U hU))

Result:
no goals

Proof state:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
h : IsClopen (⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
⊢ IsOpen (closure U)

Tactic:
rw [← (closure U).preimage_image_eq Subtype.coe_injective,
  ← h.1.isClosedEmbedding_subtypeVal.closure_image_eq U]

Result:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
h : IsClopen (⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
⊢ IsOpen ((fun a => ↑a) ⁻¹' closure (Subtype.val '' U))

Proof state:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
have h : IsClopen (i ⁻¹' (Set.range f)) :=
  ⟨IsClosed.preimage i.hom.continuous (isCompact_range f.hom.continuous).isClosed,
    IsOpen.preimage i.hom.continuous hi.isOpen_range⟩

Result:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
h : IsClopen (⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
⊢ IsOpen (closure U)
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_of_nmem_closure (h : x ∉ closure s) : HasFDerivWithinAt f f' s x :=
  .of_nhdsWithin_eq_bot <| eq_bot_mono (nhdsWithin_mono _ diff_subset) <| by
    rwa [mem_closure_iff_nhdsWithin_neBot, not_neBot] at h

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : x ∉ closure s
⊢ 𝓝[s] x = ⊥

Tactic:
rwa [mem_closure_iff_nhdsWithin_neBot, not_neBot] at h

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_add_right (h : a ∣ b) : a ∣ b + c ↔ a ∣ c

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c

Tactic:
exact dvd_add_left h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldlM_subtype [Monad m] {p : α → Prop} {l : List { x // p x }}
    {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
    l.foldlM f x = l.unattach.foldlM g x

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
l : List { x // p x }
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ List.foldlM f x l = List.foldlM g x l.unattach

Tactic:
unfold unattach

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
l : List { x // p x }
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ List.foldlM f x l = List.foldlM g x (map (fun x => x.val) l)

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
f : β → { x // p x } → m β
g : β → α → m β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, List.foldlM f x l = List.foldlM g x (map (fun x => x.val) l)
x : β
⊢ List.foldlM f x (a :: l) = List.foldlM g x (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
f : β → { x // p x } → m β
g : β → α → m β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
x : β
⊢ List.foldlM f x [] = List.foldlM g x (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
l : List { x // p x }
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ List.foldlM f x l = List.foldlM g x (map (fun x => x.val) l)

Tactic:
induction l generalizing x with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp, norm_cast]
lemma coe_complexBasis : ⇑(complexBasis α) = ((⇑) : AddChar α ℂ → α → ℂ)

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
⊢ ⇑(complexBasis α) = DFunLike.coe

Tactic:
rw [complexBasis, coe_basisOfLinearIndependentOfCardEqFinrank]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lt_trans [LT α]
    [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
    {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃

Proof state:
α : Type u_1
inst✝ : LT α
i₁ : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
l₁ l₂ l₃ : List α
h₁ : Lex (fun x1 x2 => x1 < x2) l₁ l₂
h₂ : Lex (fun x1 x2 => x1 < x2) l₂ l₃
⊢ Lex (fun x1 x2 => x1 < x2) l₁ l₃

Tactic:
exact lex_trans (fun h₁ h₂ => i₁.trans h₁ h₂) h₁ h₂

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
i₁ : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
l₁ l₂ l₃ : List α
h₁ : l₁ < l₂
h₂ : l₂ < l₃
⊢ l₁ < l₃

Tactic:
simp only [instLT, List.lt] at h₁ h₂ ⊢

Result:
α : Type u_1
inst✝ : LT α
i₁ : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
l₁ l₂ l₃ : List α
h₁ : Lex (fun x1 x2 => x1 < x2) l₁ l₂
h₂ : Lex (fun x1 x2 => x1 < x2) l₂ l₃
⊢ Lex (fun x1 x2 => x1 < x2) l₁ l₃
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma ofArrows.exists : ∃ (i : I) (h : W ⟶ Y i), g = h ≫ f i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ ∃ i h, g = h ≫ f i

Tactic:
obtain ⟨_, h, _, ⟨i⟩, rfl⟩ := hg

Result:
case intro.intro.intro.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y✝ : I → C
f : (i : I) → Y✝ i ⟶ X
W Y : C
i : I
h : W ⟶ Y✝ i
⊢ ∃ i_1 h_1, h ≫ f i = h_1 ≫ f i_1

Proof state:
case intro.intro.intro.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y✝ : I → C
f : (i : I) → Y✝ i ⟶ X
W Y : C
i : I
h : W ⟶ Y✝ i
⊢ ∃ i_1 h_1, h ≫ f i = h_1 ≫ f i_1

Tactic:
exact ⟨i, h, rfl⟩

Result:
no goals
-- Mathlib/SetTheory/Cardinal/UnivLE.lean
theorem univLE_total : UnivLE.{u, v} ∨ UnivLE.{v, u}

Proof state:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}

Tactic:
apply le_total

Result:
no goals

Proof state:
⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}

Tactic:
simp_rw [univLE_iff_cardinal_le]

Result:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_X :
    (X : R[X]).smeval x = x ^ 1

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ X.smeval x = x ^ 1

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_X_index, one_smul]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp]
lemma toKaehler_cotangentSpaceBasis (i) :
    P.toExtension.toKaehler (P.cotangentSpaceBasis i) = D R S (P.val i)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i : P.vars
⊢ P.toExtension.toKaehler (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)) = (D R S) (P.val i)

Tactic:
exact (KaehlerDifferential.mapBaseChange_tmul ..).trans (by simp)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i : P.vars
⊢ 1 • (KaehlerDifferential.map R R P.toExtension.Ring S) ((D R P.Ring) (X i)) = (D R S) (P.val i)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i : P.vars
⊢ P.toExtension.toKaehler (P.cotangentSpaceBasis i) = (D R S) (P.val i)

Tactic:
rw [cotangentSpaceBasis_apply]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i : P.vars
⊢ P.toExtension.toKaehler (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)) = (D R S) (P.val i)
-- Mathlib/Data/Finsupp/Basic.lean
theorem prod_equivMapDomain [CommMonoid N] (f : α ≃ β) (l : α →₀ M) (g : β → M → N) :
    prod (equivMapDomain f l) g = prod l (fun a m => g (f a) m)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α ≃ β
l : α →₀ M
g : β → M → N
⊢ (equivMapDomain f l).prod g = l.prod fun a m => g (f a) m

Tactic:
simp [prod, equivMapDomain]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem factorization_factorial_eq_zero_of_lt (h : n < p) : (factorial n).factorization p = 0

Proof state:
p n : ℕ
h : n < p
⊢ n !.factorization p = 0

Tactic:
induction' n with n hn

Result:
case zero
p n : ℕ
h : 0 < p
⊢ 0!.factorization p = 0

case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ (n + 1)!.factorization p = 0

Proof state:
case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ (n + 1)!.factorization p = 0

Tactic:
rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
  Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]

Result:
no goals

Proof state:
case zero
p n : ℕ
h : 0 < p
⊢ 0!.factorization p = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem le_trailingDegree_mul : p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Proof state:
case intro.mk.intro
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ ↑(i, j).1 + ↑(i, j).2 = ↑n

Tactic:
rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ (p * q).support
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n

Tactic:
rw [mem_support_iff, coeff_mul] at hn

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n

Proof state:
case intro.mk.intro
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n

Tactic:
refine
  (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
        (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_

Result:
case intro.mk.intro
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ ↑(i, j).1 + ↑(i, j).2 = ↑n

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
refine Finset.le_min fun n hn => ?_

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ (p * q).support
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n

Tactic:
obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn

Result:
case intro.mk.intro
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n
-- Mathlib/Order/Iterate.lean
theorem seq_lt_seq_of_lt_of_le (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0)
    (hx : ∀ k < n, x (k + 1) < f (x k)) (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n < y n

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n

Tactic:
cases n

Result:
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n✝ : ℕ
hx : ∀ (k : ℕ), k < n✝ + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n✝ + 1 → f (y k) ≤ y (k + 1)
⊢ x (n✝ + 1) < y (n✝ + 1)

Proof state:
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n✝ : ℕ
hx : ∀ (k : ℕ), k < n✝ + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n✝ + 1 → f (y k) ≤ y (k + 1)
⊢ x (n✝ + 1) < y (n✝ + 1)

Tactic:
exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_eq_head?_reverse {xs : List α} : xs.getLast? = xs.reverse.head?

Proof state:
α : Type u_1
xs : List α
⊢ xs.getLast? = xs.reverse.head?

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldl_subtype' {p : α → Prop} {l : Array { x // p x }}
    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) (h : stop = l.size) :
    l.foldl f x 0 stop = l.unattach.foldl g x

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x l.unattach

Tactic:
rwa [foldl_subtype]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
h : stop = l.size
⊢ foldl f x l 0 stop = foldl g x l.unattach

Tactic:
subst h

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x l.unattach
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem cons_append_cons_perm {a b : α} {as bs : List α} :
    a :: as ++ b :: bs ~ b :: as ++ a :: bs

Proof state:
α : Type u_1
a b : α
as bs : List α
⊢ a :: as ++ b :: bs ~ b :: as ++ a :: bs

Tactic:
suffices [[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten by simpa

Result:
α : Type u_1
a b : α
as bs : List α
⊢ [[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten

Proof state:
case h
α : Type u_1
a b : α
as bs : List α
⊢ [[a], as, [b], bs] ~ [[b], as, [a], bs]

Tactic:
calc
  [[a], as, [b], bs] ~ [as, [a], [b], bs] := Perm.swap as [a] _
  _ ~ [as, [b], [a], bs] := Perm.cons _ (Perm.swap [b] [a] _)
  _ ~ [[b], as, [a], bs] := Perm.swap [b] as _

Result:
no goals

Proof state:
α : Type u_1
a b : α
as bs : List α
⊢ [[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten

Tactic:
apply Perm.flatten

Result:
case h
α : Type u_1
a b : α
as bs : List α
⊢ [[a], as, [b], bs] ~ [[b], as, [a], bs]

Proof state:
α : Type u_1
a b : α
as bs : List α
this : [[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten
⊢ a :: as ++ b :: bs ~ b :: as ++ a :: bs

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
lemma nnrealPart_sub_nnrealPart_neg (f : C_c(α, ℝ)) :
    (nnrealPart f).toReal - (nnrealPart (-f)).toReal = f

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
⊢ f.nnrealPart.toReal - (-f).nnrealPart.toReal = f

Tactic:
ext x

Result:
case h
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
x : α
⊢ (f.nnrealPart.toReal - (-f).nnrealPart.toReal) x = f x

Proof state:
case h
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
x : α
⊢ (f.nnrealPart.toReal - (-f).nnrealPart.toReal) x = f x

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem IsMarkovKernel.comapRight (κ : Kernel α β) (hf : MeasurableEmbedding f)
    (hκ : ∀ a, κ a (Set.range f) = 1) : IsMarkovKernel (comapRight κ hf)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ ((κ.comapRight hf) a) Set.univ = 1

Tactic:
rw [comapRight_apply' κ hf a MeasurableSet.univ]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (f '' Set.univ) = 1

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (f '' Set.univ) = 1

Tactic:
simp only [Set.image_univ, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (Set.range f) = 1

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
⊢ IsMarkovKernel (κ.comapRight hf)

Tactic:
refine ⟨fun a => ⟨?_⟩⟩

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ ((κ.comapRight hf) a) Set.univ = 1

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (Set.range f) = 1

Tactic:
exact hκ a

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem coe_top_lt [OrderTop α] : (⊤ : α) < x ↔ x = ⊤

Proof state:
α : Type u_1
inst✝¹ : Preorder α
x : WithTop α
inst✝ : OrderTop α
⊢ ↑⊤ < x ↔ x = ⊤

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem trivial_say : trivial.sat t

Proof state:
t : Int
⊢ trivial.sat t = true

Tactic:
simp [sat, trivial]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_lxor (m n k) : testBit (Int.xor m n) k = xor (testBit m k) (testBit n k)

Proof state:
m n : ℤ
k : ℕ
⊢ (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)

Tactic:
rw [← bitwise_xor, testBit_bitwise]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_id_fun : map (id : α → α) = id

Proof state:
case h
α : Type u_1
l : List α
⊢ map id l = id l

Tactic:
induction l <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
⊢ map id = id

Tactic:
funext l

Result:
case h
α : Type u_1
l : List α
⊢ map id l = id l
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_zero : normalizedFactors (0 : α) = 0

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
⊢ normalizedFactors 0 = 0

Tactic:
simp [normalizedFactors, factors]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_to_int [AddGroupWithOne α] (n : PosNum) : ((n : ℤ) : α) = n

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : PosNum
⊢ ↑↑n = ↑n

Tactic:
rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) :
    (a.cast h)[i] = a[i]

Proof state:
case mk
α : Type u_1
n m : Nat
h : n = m
i : Nat
hi : i < m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (Vector.cast h { toArray := toArray✝, size_toArray := size_toArray✝ })[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
a : Vector α n
h : n = m
i : Nat
hi : i < m
⊢ (Vector.cast h a)[i] = a[i]

Tactic:
cases a

Result:
case mk
α : Type u_1
n m : Nat
h : n = m
i : Nat
hi : i < m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (Vector.cast h { toArray := toArray✝, size_toArray := size_toArray✝ })[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]