harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_atTop_zero_of_tsum_ne_top {f : ℕ → ℝ≥0∞} (hf : ∑' x, f x ≠ ∞) :
    Tendsto f atTop (𝓝 0)

Proof state:
f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
exact tendsto_cofinite_zero_of_tsum_ne_top hf

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ⊤
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [← Nat.cofinite_eq_atTop]

Result:
f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)
-- Mathlib/Algebra/Quaternion.lean
theorem sq_eq_neg_normSq : a ^ 2 = -normSq a ↔ a.re = 0

Proof state:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = -↑(normSq a) ↔ star a = -a

Tactic:
rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
⊢ 0 ^ 2 = -↑(normSq 0) ↔ star 0 = -0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(normSq a) ↔ star a = -a

Tactic:
obtain rfl | hq0 := eq_or_ne a 0

Result:
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
⊢ 0 ^ 2 = -↑(normSq 0) ↔ star 0 = -0

case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = -↑(normSq a) ↔ star a = -a

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(normSq a) ↔ a.re = 0

Tactic:
simp_rw [← star_eq_neg]

Result:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(normSq a) ↔ star a = -a
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem circleIntegral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {s : Set ℂ}
    (hs : s.Countable) (hw : w ∈ ball c R) {f : ℂ → ℂ} (hc : ContinuousOn f (closedBall c R))
    (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
    (∮ z in C(c, R), f z / (z - w)) = 2 * π * I * f w

Proof state:
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
f : ℂ → ℂ
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, R), f z / (z - w)) = 2 * ↑π * I * f w

Tactic:
simpa only [smul_eq_mul, div_eq_inv_mul] using
  circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem Matrix.toBilin_comp (M : Matrix n n R₁) (P Q : Matrix n o R₁) :
    (Matrix.toBilin b M).comp (toLin c b P) (toLin c b Q) = Matrix.toBilin c (Pᵀ * M * Q)

Proof state:
case H
R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ ((((toLinearMap₂ b b) M).comp ((toLin c b) P) ((toLin c b) Q)) x) y =
    ((((toLinearMap₂ b b) M).compl₁₂ ((toLin c b) P) ((toLin c b) Q)) x) y

Tactic:
simp

Result:
no goals

Proof state:
R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
⊢ ((toBilin b) M).comp ((toLin c b) P) ((toLin c b) Q) = (toBilin c) (Pᵀ * M * Q)

Tactic:
ext x y

Result:
case H
R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ ((((toBilin b) M).comp ((toLin c b) P) ((toLin c b) Q)) x) y = (((toBilin c) (Pᵀ * M * Q)) x) y

Proof state:
case H
R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ ((((toBilin b) M).comp ((toLin c b) P) ((toLin c b) Q)) x) y = (((toBilin c) (Pᵀ * M * Q)) x) y

Tactic:
rw [Matrix.toBilin, BilinForm.toMatrix, Matrix.toBilin, BilinForm.toMatrix, toMatrix₂_symm,
  toMatrix₂_symm, ← Matrix.toLinearMap₂_compl₁₂ b b c c]

Result:
case H
R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
x y : M₂'
⊢ ((((toLinearMap₂ b b) M).comp ((toLin c b) P) ((toLin c b) Q)) x) y =
    ((((toLinearMap₂ b b) M).compl₁₂ ((toLin c b) P) ((toLin c b) Q)) x) y
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
@[simp]
lemma degree_mul : degree (p * q) = degree p + degree q :=
  letI := Classical.decEq R
  if hp0 : p = 0 then by simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
  else
    if hq0 : q = 0 then by simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]
    else degree_mul' <| mul_ne_zero (mt leadingCoeff_eq_zero.1 hp0) (mt leadingCoeff_eq_zero.1 hq0)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq0 : q = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem neg (q : ℚ) : padicValRat p (-q) = padicValRat p q

Proof state:
p : ℕ
q : ℚ
⊢ padicValRat p (-q) = padicValRat p q

Tactic:
simp [padicValRat, padicValInt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ filter p l₁ <+ filter p l₂

Tactic:
rw [← filterMap_eq_filter]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ filterMap (Option.guard fun x => p x = true) l₁ <+ filterMap (Option.guard fun x => p x = true) l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ filterMap (Option.guard fun x => p x = true) l₁ <+ filterMap (Option.guard fun x => p x = true) l₂

Tactic:
apply s.filterMap

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
lemma counitForward_counitBackward (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v)
    (s : CostructuredArrow yoneda A) : counitForward F s ∘ counitBackward F s = id :=
  funext fun p => OverArrows.ext <| YonedaCollection.ext (by simp) (by simp [counitBackward])

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ F.map (eqToHom ⋯) (YonedaCollection.snd (id p).val) =
    YonedaCollection.snd ((counitForward F s ∘ counitBackward F s) p).val

Tactic:
simp [counitBackward]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ YonedaCollection.fst ((counitForward F s ∘ counitBackward F s) p).val = YonedaCollection.fst (id p).val

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
    l.toArray.allM p = l.allM p

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
⊢ allM p l.toArray = List.allM p l

Tactic:
rw [← allM_toList]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_reverse (l : Vector α n) (f : α → β → β) (b) :
    l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
  (foldl_reverse ..).symm.trans <| by simp

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β → β
b : β
⊢ foldl (fun y x => f x y) b l.reverse.reverse = foldl (fun x y => f y x) b l

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_congr {x y : ∀ i, π i} (f : (∀ i, π i) → ℝ≥0∞)
    (h : ∀ i ∉ s, x i = y i) :
    (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
x y : (i : δ) → π i
f : ((i : δ) → π i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
⊢ (∫⁻ (y : (i : { x // x ∈ s }) → π ↑i), f fun i => if hi : i ∈ s then y ⟨i, hi⟩ else x i ∂Measure.pi fun i => μ ↑i) =
    ∫⁻ (y_1 : (i : { x // x ∈ s }) → π ↑i), f fun i => if hi : i ∈ s then y_1 ⟨i, hi⟩ else y i ∂Measure.pi fun i => μ ↑i

Tactic:
rcongr

Result:
case e_f.h.e_a.h.e_e.h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
x y : (i : δ) → π i
f : ((i : δ) → π i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
x✝² : (i : { x // x ∈ s }) → π ↑i
x✝¹ : δ
x✝ : x✝¹ ∉ s
⊢ x x✝¹ = y x✝¹

Proof state:
case e_f.h.e_a.h.e_e.h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
x y : (i : δ) → π i
f : ((i : δ) → π i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
x✝² : (i : { x // x ∈ s }) → π ↑i
x✝¹ : δ
x✝ : x✝¹ ∉ s
⊢ x x✝¹ = y x✝¹

Tactic:
exact h _ ‹_›

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
x y : (i : δ) → π i
f : ((i : δ) → π i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
⊢ (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y

Tactic:
dsimp [lmarginal, updateFinset_def]

Result:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
s : Finset δ
x y : (i : δ) → π i
f : ((i : δ) → π i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
⊢ (∫⁻ (y : (i : { x // x ∈ s }) → π ↑i), f fun i => if hi : i ∈ s then y ⟨i, hi⟩ else x i ∂Measure.pi fun i => μ ↑i) =
    ∫⁻ (y_1 : (i : { x // x ∈ s }) → π ↑i), f fun i => if hi : i ∈ s then y_1 ⟨i, hi⟩ else y i ∂Measure.pi fun i => μ ↑i
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem tan_angle_add_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y = 0) :
    Real.tan (angle x (x + y)) * ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x + y)) * ‖x‖ = ‖y‖

Tactic:
rw [tan_angle_add_of_inner_eq_zero h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖

Tactic:
rcases h0 with (h0 | h0) <;> simp [h0]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem pluennecke_ruzsa_inequality_pow_div_pow_div (hA : A.Nonempty) (B : Finset G) (m n : ℕ) :
    #(B ^ m / B ^ n) ≤ (#(A / B) / #A : ℚ≥0) ^ (m + n) * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
rw [← card_inv, inv_div', ← inv_pow, ← inv_pow, div_eq_mul_inv A]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B⁻¹ ^ m / B⁻¹ ^ n)) ≤ (↑(#(A * B⁻¹)) / ↑(#A)) ^ (m + n) * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B⁻¹ ^ m / B⁻¹ ^ n)) ≤ (↑(#(A * B⁻¹)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
exact pluennecke_ruzsa_inequality_pow_div_pow_mul hA _ _ _

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive] lemma Left.min_le_max_of_mul_le_mul
    [MulLeftStrictMono α] [MulRightMono α]
    (h : a * b ≤ c * d) : min a b ≤ max c d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
exact mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ a ⊓ b ≤ c ⊔ d

Tactic:
simp_rw [min_le_iff, le_max_iff]

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
-- Mathlib/NumberTheory/PrimeCounting.lean
theorem surjective_primeCounting : Function.Surjective π

Proof state:
⊢ Function.Surjective (π ∘ fun n => n - 1)

Tactic:
convert surjective_primeCounting'

Result:
case h.e'_3

⊢ (π ∘ fun n => n - 1) = π'

Proof state:
case h.e'_3.h
x✝ : ℕ
⊢ (π ∘ fun n => n - 1) x✝ = π' x✝

Tactic:
exact primeCounting_sub_one _

Result:
no goals

Proof state:
⊢ Function.Surjective π

Tactic:
suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp

Result:
⊢ Function.Surjective (π ∘ fun n => n - 1)

Proof state:
case h.e'_3

⊢ (π ∘ fun n => n - 1) = π'

Tactic:
ext

Result:
case h.e'_3.h
x✝ : ℕ
⊢ (π ∘ fun n => n - 1) x✝ = π' x✝
-- Mathlib/Order/Bounds/Basic.lean
theorem IsLUB.insert [SemilatticeSup γ] (a) {b} {s : Set γ} (hs : IsLUB s b) :
    IsLUB (insert a s) (a ⊔ b)

Proof state:
γ : Type v
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB (insert a s) (a ⊔ b)

Tactic:
rw [insert_eq]

Result:
γ : Type v
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)

Proof state:
γ : Type v
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)

Tactic:
exact isLUB_singleton.union hs

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem prod_top (s : Subsemiring R) : s.prod (⊤ : Subsemiring S) = s.comap (RingHom.fst R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Subsemiring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (RingHom.fst R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem exists_coprime_of_gcd_pos {a : ℤ√d} (hgcd : 0 < Int.gcd a.re a.im) :
    ∃ b : ℤ√d, a = ((Int.gcd a.re a.im : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im

Proof state:
case intro.intro.intro.intro.refine_1
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ a = ↑↑(a.re.gcd a.im) * { re := re, im := im }

Tactic:
rw [smul_val, ← Hre, ← Him]

Result:
no goals

Proof state:
case intro.intro.intro.intro
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im

Tactic:
refine ⟨⟨re, im⟩, ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ a = ↑↑(a.re.gcd a.im) * { re := re, im := im }

case intro.intro.intro.intro.refine_2
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ IsCoprime { re := re, im := im }.re { re := re, im := im }.im

Proof state:
case intro.intro.intro.intro
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = re * ↑(a.re.gcd a.im)
Him : a.im = im * ↑(a.re.gcd a.im)
⊢ ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im

Tactic:
rw [mul_comm] at Hre Him

Result:
case intro.intro.intro.intro
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im

Proof state:
case intro.intro.intro.intro.refine_2
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ IsCoprime { re := re, im := im }.re { re := re, im := im }.im

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, H1]

Result:
no goals

Proof state:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
⊢ ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im

Tactic:
obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd

Result:
case intro.intro.intro.intro
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = re * ↑(a.re.gcd a.im)
Him : a.im = im * ↑(a.re.gcd a.im)
⊢ ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im
-- Mathlib/Topology/Algebra/StarSubalgebra.lean
theorem isClosedEmbedding_coe (x : A) : IsClosedEmbedding ((↑) : elemental R x → A) where
  eq_induced := rfl
  injective := Subtype.coe_injective
  isClosed_range

Proof state:
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : IsTopologicalSemiring A
inst✝² : ContinuousStar A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x : A
⊢ IsClosed (Set.range Subtype.val)

Tactic:
simpa using isClosed R x

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_rel {k : ℕ} {R : L.Relations k} {ts : Fin k → L.Term α} :
    (R.formula ts).Realize v ↔ RelMap R fun i => (ts i).realize v :=
  BoundedFormula.realize_rel.trans (by simp)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
k : ℕ
R : L.Relations k
ts : Fin k → L.Term α
⊢ (RelMap R fun i => Term.realize (Sum.elim v default) (Term.relabel Sum.inl (ts i))) ↔
    RelMap R fun i => Term.realize v (ts i)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem getElem?_iterate (f : α → α) (a : α) :
    ∀ (n i : ℕ), i < n → (iterate f a n)[i]? = f^[i] a
  | n + 1, 0    , _ => by simp
  | n + 1, i + 1, h => by simp [getElem?_iterate f (f a) n i (by simpa using h)]

Proof state:
α : Type u_1
f : α → α
a : α
n : ℕ
x✝ : 0 < n + 1
⊢ (iterate f a (n + 1))[0]? = some (f^[0] a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ (iterate f a (n + 1))[i + 1]? = some (f^[i + 1] a)

Tactic:
simp [getElem?_iterate f (f a) n i (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ i < n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem refl [Monoid M] (x : M) : x ~ᵤ x :=
  ⟨1, by simp⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
⊢ x * ↑1 = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l

Proof state:
α : Type u_1
a : α
l : List α
⊢ [a] <+ l ↔ a ∈ l

Tactic:
refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩

Result:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ [a] <+ l

Proof state:
case intro.intro
α : Type u_1
a : α
w✝¹ w✝ : List α
h : a ∈ w✝¹ ++ a :: w✝
⊢ [a] <+ w✝¹ ++ a :: w✝

Tactic:
exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ [a] <+ l

Tactic:
obtain ⟨_, _, rfl⟩ := append_of_mem h

Result:
case intro.intro
α : Type u_1
a : α
w✝¹ w✝ : List α
h : a ∈ w✝¹ ++ a :: w✝
⊢ [a] <+ w✝¹ ++ a :: w✝
-- Mathlib/Computability/Halting.lean
theorem rice₂ (C : Set Code) (H : ∀ cf cg, eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)) :
    (ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ

Proof state:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ f.eval ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun c => c ∈ C

Tactic:
obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
  Computable.const _

Result:
no goals

Proof state:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ

Tactic:
classical exact
    have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f =>
      ⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
    ⟨fun h =>
      or_iff_not_imp_left.2 fun C0 =>
        Set.eq_univ_of_forall fun cg =>
          let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
          (hC _).2 <|
            rice (eval '' C) (h.of_eq hC)
              (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
              (Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
      fun h => by {
        obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
          Computable.const _}⟩

Result:
no goals

Proof state:
C : Set Code
H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ

Tactic:
exact
have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f =>
⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
⟨fun h =>
or_iff_not_imp_left.2 fun C0 =>
Set.eq_univ_of_forall fun cg =>
let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
(hC _).2 <|
  rice (eval '' C) (h.of_eq hC)
    (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
    (Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
fun h => by {
obtain rfl | rfl := h <;> simpa [ComputablePred, Set.mem_empty_iff_false] using
Computable.const _}⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_mono_measure (f : α → ε) (hμν : ν ≪ μ) :
    eLpNormEssSup f ν ≤ eLpNormEssSup f μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ essSup (fun x => ‖f x‖ₑ) ν ≤ essSup (fun x => ‖f x‖ₑ) μ

Tactic:
exact essSup_mono_measure hμν

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ eLpNormEssSup f ν ≤ eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ essSup (fun x => ‖f x‖ₑ) ν ≤ essSup (fun x => ‖f x‖ₑ) μ