harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem verschiebung_frobenius [CharP R p] (x : 𝕎 R) : verschiebung (frobenius x) = x * p

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ verschiebung (frobenius x) = x * ↑p

Tactic:
ext ⟨i⟩

Result:
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (verschiebung (frobenius x)).coeff 0 = (x * ↑p).coeff 0

case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ (verschiebung (frobenius x)).coeff (n✝ + 1) = (x * ↑p).coeff (n✝ + 1)

Proof state:
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (verschiebung (frobenius x)).coeff 0 = (x * ↑p).coeff 0

Tactic:
rw [mul_charP_coeff_zero, verschiebung_coeff_zero]

Result:
no goals

Proof state:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ (verschiebung (frobenius x)).coeff (n✝ + 1) = (x * ↑p).coeff (n✝ + 1)

Tactic:
rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem xor_comm (x y : Nat) : x ^^^ y = y ^^^ x

Proof state:
case pred
x y : Nat
⊢ ∀ (i : Nat), (x ^^^ y).testBit i = (y ^^^ x).testBit i

Tactic:
simp [Bool.xor_comm]

Result:
no goals

Proof state:
x y : Nat
⊢ x ^^^ y = y ^^^ x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y : Nat
⊢ ∀ (i : Nat), (x ^^^ y).testBit i = (y ^^^ x).testBit i
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma prop_iterationFunctor_map_succ (j : κ.ord.toType) :
    (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE (Order.le_succ j)))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
j : κ.ord.toType
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

Tactic:
have := hasIterationOfShape I κ

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
j : κ.ord.toType
this : HasIterationOfShape κ.ord.toType C
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
j : κ.ord.toType
this : HasIterationOfShape κ.ord.toType C
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

Tactic:
have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
j : κ.ord.toType
this✝ : HasIterationOfShape κ.ord.toType C
this : NoMaxOrder κ.ord.toType
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
j : κ.ord.toType
this✝ : HasIterationOfShape κ.ord.toType C
this : NoMaxOrder κ.ord.toType
⊢ (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

Tactic:
exact (succStruct I κ).prop_iterationFunctor_map_succ j (not_isMax j)

Result:
no goals
-- Mathlib/NumberTheory/FermatPsp.lean
theorem AB_id_helper (b p : ℕ) (_ : 2 ≤ b) (hp : Odd p) :
    (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Proof state:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Tactic:
convert Nat.div_mul_div_comm q₁ q₂ using 2 <;> rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]

Result:
case h.e'_3.h.e'_5
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p) ^ 2 - 1 ^ 2

Proof state:
case h.e'_3.h.e'_5
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p) ^ 2 - 1 ^ 2

Tactic:
ring_nf

Result:
no goals

Proof state:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Tactic:
have q₁ : b - 1 ∣ b ^ p - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p

Result:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Proof state:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ b + 1 ∣ b ^ p + 1

Tactic:
simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1

Result:
no goals

Proof state:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
⊢ b - 1 ∣ b ^ p - 1

Tactic:
simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p

Result:
no goals

Proof state:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Tactic:
have q₂ : b + 1 ∣ b ^ p + 1 := by simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1

Result:
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
-- Mathlib/CategoryTheory/Category/ULift.lean
theorem eqToHom_down {X Y : AsSmall C} (h : X = Y) :
    (eqToHom h).down = eqToHom (congrArg ULift.down h)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : AsSmall C
⊢ (eqToHom ⋯).down = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : AsSmall C
h : X = Y
⊢ (eqToHom h).down = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : AsSmall C
⊢ (eqToHom ⋯).down = eqToHom ⋯
-- Mathlib/Order/RelSeries.lean
@[simp]
lemma head_singleton {r : Rel α α} (x : α) : (singleton r x).head = x

Proof state:
α : Type u_1
r : Rel α α
x : α
⊢ (singleton r x).head = x

Tactic:
simp [singleton, head]

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem support_subset_support_matPolyEquiv (m : Matrix n n R[X]) (i j : n) :
    support (m i j) ⊆ support (matPolyEquiv m)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
⊢ (m i j).support ⊆ (matPolyEquiv m).support

Tactic:
intro k

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∈ (m i j).support → k ∈ (matPolyEquiv m).support

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ (m i j).coeff k = 0

Tactic:
rw [← matPolyEquiv_coeff_apply, hk]

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ 0 i j = 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∉ (matPolyEquiv m).support → k ∉ (m i j).support

Tactic:
simp only [not_mem_support_iff]

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ (matPolyEquiv m).coeff k = 0 → (m i j).coeff k = 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ (matPolyEquiv m).coeff k = 0 → (m i j).coeff k = 0

Tactic:
intro hk

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ (m i j).coeff k = 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∈ (m i j).support → k ∈ (matPolyEquiv m).support

Tactic:
contrapose

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∉ (matPolyEquiv m).support → k ∉ (m i j).support

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ 0 i j = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toOpen_germ (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) :
    toOpen R U ≫ (structureSheaf R).presheaf.germ U x hx = toStalk R x

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ toOpen R U ≫ (structureSheaf R).presheaf.germ U x hx = toStalk R x

Tactic:
rw [← toOpen_res R ⊤ U (homOfLE le_top : U ⟶ ⊤), Category.assoc, Presheaf.germ_res]

Result:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ toOpen R ⊤ ≫ germ (structureSheaf R).val ⊤ x ⋯ = toStalk R x

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ toOpen R ⊤ ≫ germ (structureSheaf R).val ⊤ x ⋯ = toStalk R x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem size_attachWith {p : α → Prop} {l : Array α} {H} : (l.attachWith p H).size = l.size

Proof state:
α : Type u_1
p : α → Prop
l : Array α
H : ∀ (x : α), x ∈ l → p x
⊢ (l.attachWith p H).size = l.size

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → p x
⊢ ({ toList := toList✝ }.attachWith p H).size = { toList := toList✝ }.size

Proof state:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → p x
⊢ ({ toList := toList✝ }.attachWith p H).size = { toList := toList✝ }.size

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem mem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∈ p.support ↔ p.coeff m ≠ 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support ↔ coeff m p ≠ 0

Tactic:
simp [support, coeff]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma piAntidiag_empty (n : μ) : piAntidiag (∅ : Finset ι) n = if n = 0 then {0} else ∅

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.piAntidiag n = if n = 0 then {0} else ∅

Tactic:
split_ifs with hn <;> simp [*]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma Indep.mem_fundCircuit_iff (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
    x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Proof state:
case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
h : e ∉ M.closure (I \ {x})
J : Set α
hJ : J ⊆ I
heJ : e ∈ M.closure J
hxJ : x ∉ J
⊢ e ∈ M.closure (I \ {x})

Tactic:
exact M.closure_subset_closure (subset_diff_singleton hJ hxJ) heJ

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
obtain rfl | hne := eq_or_ne x e

Result:
case inl
α : Type u_1
M : Matroid α
I : Set α
x : α
hI : M.Indep I
hecl : x ∈ M.closure I
heI : x ∉ I
⊢ x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})

case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Proof state:
case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x}) by
  simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm,
    (hI.diff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]

Result:
case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})

Proof state:
case inl
α : Type u_1
M : Matroid α
I : Set α
x : α
hI : M.Indep I
hecl : x ∈ M.closure I
heI : x ∉ I
⊢ x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})

Tactic:
simp [hI.diff, mem_fundCircuit]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
this : (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm,
  (hI.diff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]

Result:
no goals

Proof state:
case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})

Tactic:
refine ⟨fun h hecl ↦ (h _ diff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩

Result:
case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
h : e ∉ M.closure (I \ {x})
J : Set α
hJ : J ⊆ I
heJ : e ∈ M.closure J
hxJ : x ∉ J
⊢ e ∈ M.closure (I \ {x})
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma isClosed_iff_isUpper : IsClosed s ↔ IsUpperSet s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsClosed s ↔ IsUpperSet s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem Filter.Tendsto.uniformity_trans {l : Filter β} {f₁ f₂ f₃ : β → α}
    (h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α))
    (h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)) : Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (fun x => (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l

Tactic:
filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)
⊢ Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α)

Tactic:
refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity

Result:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (fun x => (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_triple (hxy : x ≠ y) (hyz : y ≠ z) (hxz : x ≠ z) :
    ({x, y, z} : Set α).infsep = dist x y ⊓ dist x z ⊓ dist y z

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.infsep = dist x y ⊓ dist x z ⊓ dist y z

Tactic:
simp only [infsep, einfsep_triple hxy hyz hxz, ENNReal.toReal_inf, edist_ne_top x y,
  edist_ne_top x z, edist_ne_top y z, dist_edist, Ne, inf_eq_top_iff, and_self_iff,
  not_false_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Icc_mul_Icc_subset' (a b c d : α) : Icc a b * Icc c d ⊆ Icc (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d : α
⊢ Icc a b * Icc c d ⊆ Icc (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Icc (a * c) (b * d)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Icc (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem sub_div (h : 0 < b → b < a → c ≠ 0) : (a - b) / c = a / c - b / c

Proof state:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ⊤

Tactic:
simpa using h

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹

Tactic:
exact ENNReal.sub_mul (by simpa using h)

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c

Tactic:
simp_rw [div_eq_mul_inv]

Result:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem ofReal_cinfi (f : α → ℝ) [Nonempty α] :
    ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Proof state:
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
by_cases hf : BddBelow (range f)

Result:
case pos
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : BddBelow (range f)
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

case neg
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Proof state:
case pos
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : BddBelow (range f)
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
exact
  Monotone.map_ciInf_of_continuousAt ENNReal.continuous_ofReal.continuousAt
    (fun i j hij => ENNReal.ofReal_le_ofReal hij) hf

Result:
no goals

Proof state:
case neg.intro.intro.intro
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
i : α
hy_mem : f i ∈ range f
hy_neg : f i < 0
x : ℝ≥0∞
hx : x > ⊥
⊢ ENNReal.ofReal (f i) < x

Tactic:
rwa [ENNReal.ofReal_of_nonpos hy_neg.le]

Result:
no goals

Proof state:
case neg
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
symm

Result:
case neg
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
⊢ ⨅ i, ENNReal.ofReal (f i) = ENNReal.ofReal (⨅ i, f i)

Proof state:
case neg
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
⊢ ∀ b > ⊥, ∃ i, ENNReal.ofReal (f i) < b

Tactic:
obtain ⟨y, hy_mem, hy_neg⟩ := not_bddBelow_iff.mp hf 0

Result:
case neg.intro.intro
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
y : ℝ
hy_mem : y ∈ range f
hy_neg : y < 0
⊢ ∀ b > ⊥, ∃ i, ENNReal.ofReal (f i) < b

Proof state:
case neg
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
⊢ ⨅ i, ENNReal.ofReal (f i) = ENNReal.ofReal (⨅ i, f i)

Tactic:
rw [Real.iInf_of_not_bddBelow hf, ENNReal.ofReal_zero, ← ENNReal.bot_eq_zero, iInf_eq_bot]

Result:
case neg
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
⊢ ∀ b > ⊥, ∃ i, ENNReal.ofReal (f i) < b

Proof state:
case neg.intro.intro
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
y : ℝ
hy_mem : y ∈ range f
hy_neg : y < 0
⊢ ∀ b > ⊥, ∃ i, ENNReal.ofReal (f i) < b

Tactic:
obtain ⟨i, rfl⟩ := mem_range.mpr hy_mem

Result:
case neg.intro.intro.intro
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
i : α
hy_mem : f i ∈ range f
hy_neg : f i < 0
⊢ ∀ b > ⊥, ∃ i, ENNReal.ofReal (f i) < b

Proof state:
case neg.intro.intro.intro
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
i : α
hy_mem : f i ∈ range f
hy_neg : f i < 0
⊢ ∀ b > ⊥, ∃ i, ENNReal.ofReal (f i) < b

Tactic:
refine fun x hx => ⟨i, ?_⟩

Result:
case neg.intro.intro.intro
α : Type u_1
f : α → ℝ
inst✝ : Nonempty α
hf : ¬BddBelow (range f)
i : α
hy_mem : f i ∈ range f
hy_neg : f i < 0
x : ℝ≥0∞
hx : x > ⊥
⊢ ENNReal.ofReal (f i) < x
-- Mathlib/Data/ENat/Lattice.lean
lemma sSup_eq_top_of_infinite (h : s.Infinite) : sSup s = ⊤

Proof state:
case top
s : Set ℕ∞
h : s.Infinite
hx : ⊤ < ⊤
⊢ ∃ a ∈ s, ⊤ < a

Tactic:
simp at hx

Result:
no goals

Proof state:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ s ⊆ (fun n => ↑n) '' {n | n ≤ x}

Tactic:
intro y hy

Result:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
y : ℕ∞
hy : y ∈ s
⊢ y ∈ (fun n => ↑n) '' {n | n ≤ x}

Proof state:
case h
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ ↑x
hxt : y < ⊤
⊢ y.toNat ∈ {n | n ≤ x} ∧ (fun n => ↑n) y.toNat = y

Tactic:
simp [toNat_le_of_le_coe h, LT.lt.ne_top hxt]

Result:
no goals

Proof state:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ ¬s.Infinite

Tactic:
simp only [not_infinite]

Result:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ s.Finite

Proof state:
s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤

Tactic:
apply (sSup_eq_top ..).mpr

Result:
s : Set ℕ∞
h : s.Infinite
⊢ ∀ b < ⊤, ∃ a ∈ s, b < a

Proof state:
s : Set ℕ∞
h : s.Infinite
⊢ ∀ b < ⊤, ∃ a ∈ s, b < a

Tactic:
intro x hx

Result:
s : Set ℕ∞
h : s.Infinite
x : ℕ∞
hx : x < ⊤
⊢ ∃ a ∈ s, x < a

Proof state:
case coe
s : Set ℕ∞
h : s.Infinite
x : ℕ
hx : ↑x < ⊤
⊢ ∃ a ∈ s, ↑x < a

Tactic:
contrapose! h

Result:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ ¬s.Infinite

Proof state:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
y : ℕ∞
hy : y ∈ s
⊢ y ∈ (fun n => ↑n) '' {n | n ≤ x}

Tactic:
specialize h y hy

Result:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ ↑x
⊢ y ∈ (fun n => ↑n) '' {n | n ≤ x}

Proof state:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ ↑x
hxt : y < ⊤
⊢ y ∈ (fun n => ↑n) '' {n | n ≤ x}

Tactic:
use y.toNat

Result:
case h
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ ↑x
hxt : y < ⊤
⊢ y.toNat ∈ {n | n ≤ x} ∧ (fun n => ↑n) y.toNat = y

Proof state:
s : Set ℕ∞
h : s.Infinite
x : ℕ∞
hx : x < ⊤
⊢ ∃ a ∈ s, x < a

Tactic:
cases x with
| top => simp at hx
| coe x =>
  contrapose! h
  simp only [not_infinite]
  apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
  intro y hy
  specialize h y hy
  have hxt : y < ⊤ := lt_of_le_of_lt h hx
  use y.toNat
  simp [toNat_le_of_le_coe h, LT.lt.ne_top hxt]

Result:
no goals

Proof state:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ ↑x
⊢ y ∈ (fun n => ↑n) '' {n | n ≤ x}

Tactic:
have hxt : y < ⊤ := lt_of_le_of_lt h hx

Result:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ ↑x
hxt : y < ⊤
⊢ y ∈ (fun n => ↑n) '' {n | n ≤ x}

Proof state:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ s.Finite

Tactic:
apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))

Result:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ s ⊆ (fun n => ↑n) '' {n | n ≤ x}
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma coeffs_one_of_nontrivial [Nontrivial R] : coeffs (1 : MvPolynomial σ R) = {1}

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ {1} ⊆ coeffs 1

Tactic:
simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ∃ a ∈ support 1, coeff a 1 = 1

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ coeffs 1 = {1}

Tactic:
apply Finset.Subset.antisymm coeffs_one

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ {1} ⊆ coeffs 1

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ 0 ∈ support 1 ∧ coeff 0 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ∃ a ∈ support 1, coeff a 1 = 1

Tactic:
exact ⟨0, by simp⟩

Result:
no goals