harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsPath.getVert_eq_end_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
    p.getVert i = w ↔ i = p.length

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = w ↔ i = p.length

Tactic:
have := hp.reverse.getVert_eq_start_iff (by omega : p.reverse.length - i ≤ p.reverse.length)

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.getVert i = w ↔ i = p.length

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.reverse.length - i ≤ p.reverse.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.length - i = 0 ↔ i = p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.getVert i = w ↔ i = p.length

Tactic:
simp only [length_reverse, getVert_reverse,
  show p.length - (p.length - i) = i from by omega] at this

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.getVert i = w ↔ i = p.length

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.length - (p.length - i) = i

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.getVert i = w ↔ i = p.length

Tactic:
rw [this]

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.length - i = 0 ↔ i = p.length
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive] lemma prod_sdiff_lt_prod_sdiff :
    ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Tactic:
rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
  ← prod_union, inter_comm, sdiff_union_inter]

Result:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
simpa only [inter_comm] using disjoint_sdiff_inter t s

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_symm (p₀ p₁ : P1) :
    lineMap p₀ p₁ = (lineMap p₁ p₀).comp (lineMap (1 : k) (0 : k))

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ lineMap p₀ p₁ = (lineMap p₁ p₀).comp (lineMap 1 0)

Tactic:
rw [comp_lineMap]

Result:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ lineMap p₀ p₁ = lineMap ((lineMap p₁ p₀) 1) ((lineMap p₁ p₀) 0)

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ lineMap p₀ p₁ = lineMap ((lineMap p₁ p₀) 1) ((lineMap p₁ p₀) 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem add_tsub_tsub_cancel (hac : AddLECancellable (a - c)) (h : c ≤ a) :
    a + b - (a - c) = b + c :=
  hac.tsub_eq_of_eq_add <| by rw [add_assoc, add_tsub_cancel_of_le h, add_comm]

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)

Tactic:
rw [add_assoc, add_tsub_cancel_of_le h, add_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Idempotent.lean
lemma pow (n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n) :=
  Nat.recOn n ((pow_zero a).symm ▸ one) fun n _ =>
    show a ^ n.succ * a ^ n.succ = a ^ n.succ by
      conv_rhs => rw [← h.eq]
      rw [← sq, ← sq, ← pow_mul, ← pow_mul']

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ

Tactic:
rw [← sq, ← sq, ← pow_mul, ← pow_mul']

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = a ^ n.succ

Tactic:
conv_rhs => rw [← h.eq]

Result:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b

Proof state:
case succ
a n✝ : Nat
hba : n✝ + 1 ≤ a
hb : 0 < n✝ + 1
⊢ 0 < a / (n✝ + 1)

Tactic:
simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba]

Result:
no goals

Proof state:
b a : Nat
hba : b ≤ a
hb : 0 < b
⊢ 0 < a / b

Tactic:
cases b

Result:
case zero
a : Nat
hba : 0 ≤ a
hb : 0 < 0
⊢ 0 < a / 0

case succ
a n✝ : Nat
hba : n✝ + 1 ≤ a
hb : 0 < n✝ + 1
⊢ 0 < a / (n✝ + 1)

Proof state:
case zero
a : Nat
hba : 0 ≤ a
hb : 0 < 0
⊢ 0 < a / 0

Tactic:
contradiction

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_eq_elem_of_subsingleton [Subsingleton n] (A : Matrix n n R) (k : n) :
    det A = A k k

Proof state:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
A : Matrix n n R
k : n
⊢ A.det = A k k

Tactic:
have := uniqueOfSubsingleton k

Result:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
A : Matrix n n R
k : n
this : Unique n
⊢ A.det = A k k

Proof state:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
A : Matrix n n R
k : n
this : Unique n
⊢ A.det = A k k

Tactic:
convert det_unique A

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_self_lt_mul_self_iff : m * m < n * n ↔ m < n

Proof state:
m n : ℕ
⊢ m * m < n * n ↔ m < n

Tactic:
simp only [← Nat.not_le, mul_self_le_mul_self_iff]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
lemma exists_prime_iff :
    (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬ IsUnit x

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : ∃ x, x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
⊢ ∃ p, Prime p

Tactic:
obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀

Result:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : ∃ x, x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
f : α
hf : Irreducible f
⊢ ∃ p, Prime p

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : ∃ x, x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
f : α
hf : Irreducible f
⊢ ∃ p, Prime p

Tactic:
exact ⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x

Tactic:
refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : ∃ x, x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
⊢ ∃ p, Prime p
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iff : (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⇔ ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

Tactic:
simp only [BoundedFormula.iff, realize_inf, realize_imp, and_imp, ← iff_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem le_length_erase [LawfulBEq α] (a : α) (l : List α) : l.length - 1 ≤ (l.erase a).length

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ l.length - 1 ≤ if a ∈ l then l.length - 1 else l.length

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ l.length - 1 ≤ (l.erase a).length

Tactic:
rw [length_erase]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ l.length - 1 ≤ if a ∈ l then l.length - 1 else l.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_flatten {p : α → Prop} {L : List (List α)} :
    (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x

Proof state:
case mpr
α : Type u_1
p : α → Prop
L : List (List α)
⊢ (∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x) → ∀ (x : α) (x_1 : List α), x_1 ∈ L → x ∈ x_1 → p x

Tactic:
intros

Result:
case mpr
α : Type u_1
p : α → Prop
L : List (List α)
a✝² : ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x
x✝¹ : α
x✝ : List α
a✝¹ : x✝ ∈ L
a✝ : x✝¹ ∈ x✝
⊢ p x✝¹

Proof state:
α : Type u_1
p : α → Prop
L : List (List α)
⊢ (∀ (x : α), x ∈ L.flatten → p x) ↔ ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x

Tactic:
simp only [mem_flatten, forall_exists_index, and_imp]

Result:
α : Type u_1
p : α → Prop
L : List (List α)
⊢ (∀ (x : α) (x_1 : List α), x_1 ∈ L → x ∈ x_1 → p x) ↔ ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x

Proof state:
α : Type u_1
p : α → Prop
L : List (List α)
⊢ (∀ (x : α) (x_1 : List α), x_1 ∈ L → x ∈ x_1 → p x) ↔ ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x

Tactic:
constructor <;> (intros; solve_by_elim)

Result:
no goals

Proof state:
case mpr
α : Type u_1
p : α → Prop
L : List (List α)
a✝² : ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x
x✝¹ : α
x✝ : List α
a✝¹ : x✝ ∈ L
a✝ : x✝¹ ∈ x✝
⊢ p x✝¹

Tactic:
solve_by_elim

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.app_one_eq_ι_comp_left (s : Fork f g) : s.π.app one = s.ι ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ f

Tactic:
rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso
    (h : S.HomologyData) [S.HasHomology] :
    h.right.homologyIso = h.left.homologyIso ≪≫ h.iso

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso

Tactic:
ext

Result:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = (h.left.homologyIso.symm ≪≫ h.right.homologyIso).hom

Proof state:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = h.left.homologyIso.inv ≫ h.right.homologyIso.hom

Tactic:
rw [← leftRightHomologyComparison'_fac, leftRightHomologyComparison'_eq]

Result:
no goals

Proof state:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = (h.left.homologyIso.symm ≪≫ h.right.homologyIso).hom

Tactic:
dsimp

Result:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = h.left.homologyIso.inv ≫ h.right.homologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.right.homologyIso = h.left.homologyIso ≪≫ h.iso

Tactic:
suffices h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso by
  rw [this, Iso.self_symm_id_assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
this : h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso
⊢ h.right.homologyIso = h.left.homologyIso ≪≫ h.iso

Tactic:
rw [this, Iso.self_symm_id_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (insertMany empty l).1.getKeyD k' fallback = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (empty.insertMany l).val.getKeyD k' fallback = k

Tactic:
rw [getKeyD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_one : withTopEquiv.symm 1 = 1

Proof state:
⊢ withTopEquiv.symm 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem nnnorm_deriv_mulExpNegMulSq_le_one (hε : 0 < ε) (x : ℝ) :
    ‖deriv (mulExpNegMulSq ε) x‖₊ ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Tactic:
rw [← NNReal.coe_le_coe, coe_nnnorm]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ ↑1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ ↑1

Tactic:
exact norm_deriv_mulExpNegMulSq_le_one hε x

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_lt_of_lt_log (hy : 0 < y) (h : log x < z * log y) : x < y ^ z

Proof state:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
⊢ x < y ^ z

Tactic:
obtain hx | hx := le_or_lt x 0

Result:
case inl
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Proof state:
case inl
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

Tactic:
exact hx.trans_lt (rpow_pos_of_pos hy _)

Result:
no goals

Proof state:
case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Tactic:
exact (lt_rpow_iff_log_lt hx hy).2 h

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem le_degree {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : d ∈ f.support) :
    d ≼[m] m.degree f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn))

Tactic:
simp only [AddEquiv.apply_symm_apply, Finset.le_sup hd]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.degree f)

Tactic:
unfold degree

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn))
-- Mathlib/Topology/Constructions.lean
theorem Filter.eventually_nhdsSet_prod_iff {p : X × Y → Prop} :
    (∀ᶠ q in 𝓝ˢ (s ×ˢ t), p q) ↔
      ∀ x ∈ s, ∀ y ∈ t,
          ∃ px : X → Prop, (∀ᶠ x' in 𝓝 x, px x') ∧ ∃ py : Y → Prop, (∀ᶠ y' in 𝓝 y, py y') ∧
            ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_lt_of_lt_sub' {a b c : Nat} : b < c - a → a + b < c

Proof state:
a b c : Nat
⊢ b < c - a → a + b < c

Tactic:
rw [Nat.add_comm]

Result:
a b c : Nat
⊢ b < c - a → b + a < c

Proof state:
a b c : Nat
⊢ b < c - a → b + a < c

Tactic:
exact Nat.add_lt_of_lt_sub

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ici_subset_Ici : Ici a ⊆ Ici b ↔ b ≤ a

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ici a ⊆ Ici b ↔ b ≤ a

Tactic:
simp [← coe_subset]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem _root_.Polynomial.toLaurent_C (r : R) : toLaurent (Polynomial.C r) = C r

Proof state:
case h.e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ C r = C r * T ↑0

Tactic:
simp only [Int.ofNat_zero, T_zero, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
⊢ toLaurent (Polynomial.C r) = C r

Tactic:
convert Polynomial.toLaurent_C_mul_T 0 r

Result:
case h.e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ C r = C r * T ↑0
-- Mathlib/RingTheory/Multiplicity.lean
theorem Int.natCast_emultiplicity (a b : ℕ) :
    emultiplicity (a : ℤ) (b : ℤ) = emultiplicity a b

Proof state:
a b : ℕ
⊢ (if h : ∃ n, ¬↑a ^ (n + 1) ∣ ↑b then ↑(Nat.find h) else ⊤) = if h : ∃ n, ¬a ^ (n + 1) ∣ b then ↑(Nat.find h) else ⊤

Tactic:
congr! <;> norm_cast

Result:
no goals

Proof state:
a b : ℕ
⊢ emultiplicity ↑a ↑b = emultiplicity a b

Tactic:
unfold emultiplicity FiniteMultiplicity

Result:
a b : ℕ
⊢ (if h : ∃ n, ¬↑a ^ (n + 1) ∣ ↑b then ↑(Nat.find h) else ⊤) = if h : ∃ n, ¬a ^ (n + 1) ∣ b then ↑(Nat.find h) else ⊤
-- Mathlib/NumberTheory/FactorisationProperties.lean
lemma abundant_iff_not_perfect_and_not_deficient (hn : 0 ≠ n) :
    Abundant n ↔ ¬ Perfect n ∧ ¬ Deficient n

Proof state:
n : ℕ
hn : 0 ≠ n
⊢ n < ∑ i ∈ n.properDivisors, i ↔ ¬(∑ i ∈ n.properDivisors, i = n ∧ 0 < n) ∧ ¬∑ i ∈ n.properDivisors, i < n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hn : 0 ≠ n
⊢ n.Abundant ↔ ¬n.Perfect ∧ ¬n.Deficient

Tactic:
dsimp only [Perfect, Abundant, Deficient]

Result:
n : ℕ
hn : 0 ≠ n
⊢ n < ∑ i ∈ n.properDivisors, i ↔ ¬(∑ i ∈ n.properDivisors, i = n ∧ 0 < n) ∧ ¬∑ i ∈ n.properDivisors, i < n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLE_eq_false {o : Ordering} : o.isLE = false ↔ o = .gt

Proof state:
o : Ordering
⊢ o.isLE = false ↔ o = gt

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma div_two_lt_floor (ha : 1 ≤ a) : a / 2 < ⌊a⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊

Tactic:
refine mul_lt_floor ?_ ?_ ?_ <;> norm_num

Result:
case refine_3
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 ≤ a
⊢ 1 ≤ a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋₊

Tactic:
rw [div_eq_inv_mul]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊

Proof state:
case refine_3
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 ≤ a
⊢ 1 ≤ a

Tactic:
assumption

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π / 2)
    (hxy : x < y) : cos y < cos x :=
  cos_lt_cos_of_nonneg_of_le_pi hx₁ (hy₂.trans (by linarith)) hxy

Proof state:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ π / 2 ≤ π

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_neg (a b : Int) : tmod a (-b) = tmod a b

Proof state:
a b : Int
⊢ a.tmod (-b) = a.tmod b

Tactic:
rw [tmod_def, tmod_def, Int.tdiv_neg, Int.neg_mul_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_Iio {l : ℝ} (hf : Tendsto f atBot (𝓝 l)) (x : ℝ) :
    f.measure (Iio x) = ofReal (leftLim f x - l)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ f.measure (Iio x) = ofReal (leftLim (↑f) x - l)

Tactic:
rw [← Iic_diff_right, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
  f.measure_Iic hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
  <;> simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subset (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1) :
    ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x :=
  haveI := Classical.decEq α
  prod_subset_one_on_sdiff h (by simpa) fun _ _ => rfl

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝ : CommMonoid β
h : s₁ ⊆ s₂
hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1
this : DecidableEq α
⊢ ∀ x ∈ s₂ \ s₁, f x = 1

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_nnnorm_transpose (A : Matrix m n α) : ‖Aᵀ‖₊ = ‖A‖₊

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ (∑ y : m, ∑ x : n, ‖Aᵀ x y‖₊ ^ 2) ^ (1 / 2) = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
simp_rw [Matrix.transpose_apply]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖Aᵀ‖₊ = ‖A‖₊

Tactic:
rw [frobenius_nnnorm_def, frobenius_nnnorm_def, Finset.sum_comm]

Result:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ (∑ y : m, ∑ x : n, ‖Aᵀ x y‖₊ ^ 2) ^ (1 / 2) = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_pow (f : N ≃ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N ≃ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
simpa only [one_pow] using TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n

Result:
no goals