harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/AddCircle.lean
theorem liftIco_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ico a (a + p)) :
    liftIco p a f ↑x = f x

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ (equivIco p a) ↑x = ⟨x, hx⟩

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply]

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = (equivIco p a).symm ⟨x, hx⟩

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : (equivIco p a) ↑x = ⟨x, hx⟩
⊢ liftIco p a f ↑x = f x

Tactic:
rw [liftIco, comp_apply, this]

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : (equivIco p a) ↑x = ⟨x, hx⟩
⊢ (Ico a (a + p)).restrict f ⟨x, hx⟩ = f x

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIco p a f ↑x = f x

Tactic:
have : (equivIco p a) x = ⟨x, hx⟩ := by
  rw [Equiv.apply_eq_iff_eq_symm_apply]
  rfl

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : (equivIco p a) ↑x = ⟨x, hx⟩
⊢ liftIco p a f ↑x = f x

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = (equivIco p a).symm ⟨x, hx⟩

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : (equivIco p a) ↑x = ⟨x, hx⟩
⊢ (Ico a (a + p)).restrict f ⟨x, hx⟩ = f x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
simpa only [dist_mul_left, dist_mul_right] using dist_triangle (a₁ * a₂) (b₁ * a₂) (b₁ * b₂)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
lemma Real.multipliable_one_add_of_summable (f : ι → ℝ) (hf : Summable f) :
    Multipliable (fun n : ι => 1 + |f n|)

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
x✝ : ι
⊢ 0 < (fun n => 1 + |f n|) x✝

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Multipliable fun n => 1 + |f n|

Tactic:
refine Real.multipliable_of_summable_log (fun n => 1 + |f n|) (fun _ ↦ by positivity) ?_

Result:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Summable fun n => log ((fun n => 1 + |f n|) n)

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Summable fun n => log ((fun n => 1 + |f n|) n)

Tactic:
simpa only [forall_const] using Real.summable_log_one_add_of_summable  hf

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem pure_bindOnSupport (a : α) (f : ∀ (a' : α) (_ : a' ∈ (pure a).support), PMF β) :
    (pure a).bindOnSupport f = f a ((mem_support_pure_iff a a).mpr rfl)

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ ((pure a).bindOnSupport f) b = (f a ⋯) b

Tactic:
simp only [bindOnSupport_apply, pure_apply]

Result:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ (∑' (a_1 : α), (if a_1 = a then 1 else 0) * if h : (if a_1 = a then 1 else 0) = 0 then 0 else (f a_1 h) b) = (f a ⋯) b

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ (∑' (a_1 : α), (if a_1 = a then 1 else 0) * if h : (if a_1 = a then 1 else 0) = 0 then 0 else (f a_1 h) b) = (f a ⋯) b

Tactic:
classical
refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a _)
by_cases h : a' = a <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ (∑' (a_1 : α), (if a_1 = a then 1 else 0) * if h : (if a_1 = a then 1 else 0) = 0 then 0 else (f a_1 h) b) = (f a ⋯) b

Tactic:
refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a _)

Result:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) =
    if a' = a then (f a ⋯) b else 0

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
⊢ (pure a).bindOnSupport f = f a ⋯

Tactic:
refine PMF.ext fun b => ?_

Result:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ ((pure a).bindOnSupport f) b = (f a ⋯) b

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) =
    if a' = a then (f a ⋯) b else 0

Tactic:
by_cases h : a' = a <;> simp [h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuous_iff_continuous {F : ι → X → α} :
    Equicontinuous F ↔ Continuous (ofFun ∘ Function.swap F : X → ι →ᵤ α)

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ Equicontinuous F ↔ Continuous (⇑ofFun ∘ swap F)

Tactic:
simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem compl_compl_inf_distrib (a b : α) : (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

Tactic:
refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_

Result:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ

Tactic:
exact disjoint_compl_right

Result:
no goals

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
  disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]

Result:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_closure_singleton {x y : A} : y ∈ closure ({x} : Set A) ↔ ∃ n : ℕ, n • x = y

Proof state:
A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ y ∈ closure {x} ↔ ∃ n, n • x = y

Tactic:
rw [closure_singleton_eq, AddMonoidHom.mem_mrange]

Result:
A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y

Proof state:
A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_swap (a : Array α) (i j : Nat) {hi hj} (k : Nat) (hk : k < (a.swap i j).size) :
    (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all)

Proof state:
α : Type ?u.523232
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < (a.swap i j hi hj).size
⊢ k < a.size

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < (a.swap i j hi hj).size
⊢ (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

Tactic:
apply getElem_swap'

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.tan (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
/-- `Fₙ = 2^(2^n)+1` is prime if `3^(2^(2^n-1)) = -1 mod Fₙ` (**Pépin's test**). -/
lemma pepin_primality (n : ℕ) (h : 3 ^ (2 ^ (2 ^ n - 1)) = (-1 : ZMod (fermatNumber n))) :
    (fermatNumber n).Prime

Proof state:
case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ 3 ^ (2 ^ 2 ^ n + 1 - 1) = 1

Tactic:
rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]

Result:
no goals

Proof state:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ ((2 ^ 2 ^ n + 1 - 1) / p) ≠ 1

Tactic:
rw [Nat.add_sub_cancel, (Nat.prime_dvd_prime_iff_eq hp1 prime_two).mp (hp1.dvd_of_dvd_pow hp2),
    key, pow_succ, Nat.mul_div_cancel _ two_pos, ← pow_succ, ← key, h]

Result:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ -1 ≠ 1

Proof state:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
⊢ Prime n.fermatNumber

Tactic:
have key : 2 ^ n = 2 ^ n - 1 + 1 := (Nat.sub_add_cancel Nat.one_le_two_pow).symm

Result:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ Prime n.fermatNumber

Proof state:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ -1 ≠ 1

Tactic:
exact neg_one_ne_one

Result:
no goals

Proof state:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ ∀ (q : ℕ), Prime q → q ∣ 2 ^ 2 ^ n + 1 - 1 → 3 ^ ((2 ^ 2 ^ n + 1 - 1) / q) ≠ 1

Tactic:
intro p hp1 hp2

Result:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ ((2 ^ 2 ^ n + 1 - 1) / p) ≠ 1

Proof state:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ Prime n.fermatNumber

Tactic:
apply lucas_primality (p := 2 ^ (2 ^ n) + 1) (a := 3)

Result:
case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ 3 ^ (2 ^ 2 ^ n + 1 - 1) = 1

case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ ∀ (q : ℕ), Prime q → q ∣ 2 ^ 2 ^ n + 1 - 1 → 3 ^ ((2 ^ 2 ^ n + 1 - 1) / q) ≠ 1

Proof state:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
⊢ Prime n.fermatNumber

Tactic:
have := Fact.mk (two_lt_fermatNumber n)

Result:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
⊢ Prime n.fermatNumber
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma desc_f (j k : ι) (hjk : c.Rel j k) :
    (desc φ α hα).f j = fstX φ j _ hjk ≫ hα.hom _ j + sndX φ j ≫ α.f j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ (desc φ α hα).f j = fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j

Tactic:
apply dif_pos hjk

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j k : ι
hjk : c.Rel j k
⊢ (desc φ α hα).f j = fstX φ j k hjk ≫ hα.hom k j + sndX φ j ≫ α.f j

Tactic:
obtain rfl := c.next_eq' hjk

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ (desc φ α hα).f j = fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
-- Mathlib/Topology/MetricSpace/MetricSeparated.lean
theorem disjoint (h : AreSeparated s t) : Disjoint s t :=
  let ⟨r, r0, hr⟩ := h
  Set.disjoint_left.mpr fun x hx1 hx2 => r0 <| by simpa using hr x hx1 x hx2

Proof state:
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
h : AreSeparated s t
r : ENNReal
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
x : X
hx1 : x ∈ s
hx2 : x ∈ t
⊢ r = 0

Tactic:
simpa using hr x hx1 x hx2

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) :
    (a * b).support ⊆ a.support * b.support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
a b : MonoidAlgebra k G
⊢ (a * b).support ⊆ a.support * b.support

Tactic:
rw [MonoidAlgebra.mul_def]

Result:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
a b : MonoidAlgebra k G
⊢ (sum a fun a₁ b₁ => sum b fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)).support ⊆ a.support * b.support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
a b : MonoidAlgebra k G
⊢ (sum a fun a₁ b₁ => sum b fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)).support ⊆ a.support * b.support

Tactic:
exact support_sum.trans <| biUnion_subset.2 fun _x hx ↦
  support_sum.trans <| biUnion_subset.2 fun _y hy ↦
    support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part [IsFiniteMeasure μ]
    (a b : ℝ) (hf : Submartingale f ℱ μ) (N : ℕ) :
    (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[fun ω => (f N ω - a)⁺]

Proof state:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b - a ≤ 0
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Tactic:
exact le_trans (mul_nonpos_of_nonpos_of_nonneg hab (by positivity))
  (integral_nonneg fun ω => posPart_nonneg _)

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b - a ≤ 0
⊢ 0 ≤ ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Tactic:
by_cases hab : a < b

Result:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : ¬a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Proof state:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Tactic:
exact mul_integral_upcrossingsBefore_le_integral_pos_part_aux hf hab

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : ¬a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Tactic:
rw [not_lt, ← sub_nonpos] at hab

Result:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b - a ≤ 0
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
@[simp]
lemma codRestrictOfInjective_comp :
    i ∘ₗ LinearMap.codRestrictOfInjective f i hi hf = f

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ range i
⊢ i ∘ₗ f.codRestrictOfInjective i hi hf = f

Tactic:
ext

Result:
case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ range i
x✝ : M₁
⊢ (i ∘ₗ f.codRestrictOfInjective i hi hf) x✝ = f x✝

Proof state:
case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ range i
x✝ : M₁
⊢ (i ∘ₗ f.codRestrictOfInjective i hi hf) x✝ = f x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArray

Proof state:
case h
α : Type u_1
a : α
l : List α
⊢ (a :: l).toArray.toList = (#[a] ++ l.toArray).toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).toArray = #[a] ++ l.toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
a : α
l : List α
⊢ (a :: l).toArray.toList = (#[a] ++ l.toArray).toList
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem restrictNonposSeq_lt (n : ℕ) (hn : ¬s ≤[i \ ⋃ k ≤ n, restrictNonposSeq s i k] 0) :
    (1 / (findExistsOneDivLT s (i \ ⋃ k ≤ n, restrictNonposSeq s i k) + 1) : ℝ) <
      s (restrictNonposSeq s i n.succ)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i n.succ)

Tactic:
rw [restrictNonposSeq_succ]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))

Tactic:
apply someExistsOneDivLT_lt hn

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem mem_sSup_of_directedOn {S : Set (NonUnitalSubring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : R} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib/RingTheory/PowerBasis.lean
theorem exists_gen_dvd_sub (pb : PowerBasis A B) (b : B) : ∃ a, pb.gen ∣ b - algebraMap A B a

Proof state:
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ a, pb.gen ∣ b - (algebraMap A B) a

Tactic:
simpa [← Ideal.mem_span_singleton, ← mk_eq_zero, mk_sub, sub_eq_zero] using pb.exists_smodEq b

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Partition.lean
theorem mem_partOfVertex (v : V) : v ∈ P.partOfVertex v

Proof state:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ v ∈ P.partOfVertex v

Tactic:
obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec

Result:
case intro.intro
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right✝ : ∀ (y : Set V), (fun b => b ∈ P.parts ∧ v ∈ b) y → y = Exists.choose ⋯
left✝ : Exists.choose ⋯ ∈ P.parts
h : v ∈ Exists.choose ⋯
⊢ v ∈ P.partOfVertex v

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right✝ : ∀ (y : Set V), (fun b => b ∈ P.parts ∧ v ∈ b) y → y = Exists.choose ⋯
left✝ : Exists.choose ⋯ ∈ P.parts
h : v ∈ Exists.choose ⋯
⊢ v ∈ P.partOfVertex v

Tactic:
exact h

Result:
no goals