harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Functor/Flat.lean
theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
    (f₁ f₂ : s.pt ⟶ F.obj c.pt) (h₁ : ∀ j : J, f₁ ≫ (F.mapCone c).π.app j = s.π.app j)
    (h₂ : ∀ j : J, f₂ ≫ (F.mapCone c).π.app j = s.π.app j) : f₁ = f₂

Proof state:
case x
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j
this : c.extend g₁.right = c.extend g₂.right
⊢ ∀ (j : J), g₁.right ≫ c.π.app j = (c.extend g₁.right).π.app j

Tactic:
intro j

Result:
case x
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j
this : c.extend g₁.right = c.extend g₂.right
j : J
⊢ g₁.right ≫ c.π.app j = (c.extend g₁.right).π.app j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}  :
    (l.set i a)[j]? = l[j]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : ¬j < (l.set i a).length
⊢ l.length ≤ j

Tactic:
simp_all

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : ¬j < (l.set i a).length
⊢ (l.set i a)[j]? = l[j]?

Tactic:
rw [getElem?_eq_none (by simp_all), getElem?_eq_none (by simp_all)]

Result:
no goals

Proof state:
case pos
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ some (l.set i a)[j] = some l[j]

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
⊢ (l.set i a)[j]? = l[j]?

Tactic:
by_cases hj : j < (l.set i a).length

Result:
case pos
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ (l.set i a)[j]? = l[j]?

case neg
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : ¬j < (l.set i a).length
⊢ (l.set i a)[j]? = l[j]?

Proof state:
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : ¬j < (l.set i a).length
⊢ (l.set i a).length ≤ j

Tactic:
simp_all

Result:
no goals

Proof state:
case pos
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ (l.set i a)[j]? = l[j]?

Tactic:
rw [getElem?_eq_getElem hj, getElem?_eq_getElem (by simp_all)]

Result:
case pos
α : Type u_1
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ some (l.set i a)[j] = some l[j]
-- Mathlib/Data/Nat/Factors.lean
theorem mem_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : Coprime a b) (p : ℕ) :
    p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Proof state:
a b : ℕ
hab : a.Coprime b
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rcases a.eq_zero_or_pos with (rfl | ha)

Result:
case inl
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList

case inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Proof state:
case inr.inl
a p : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0

Tactic:
simp [(coprime_zero_right _).mp hab]

Result:
no goals

Proof state:
case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]

Result:
no goals

Proof state:
case inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Result:
case inr.inl
a p : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0

case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Proof state:
case inl
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList

Tactic:
simp [(coprime_zero_left _).mp hab]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift'_iInf_of_map_univ {f : ι → Filter α} {g : Set α → Set β}
    (hg : ∀ {s t}, g (s ∩ t) = g s ∩ g t) (hg' : g univ = univ) :
    (iInf f).lift' g = ⨅ i, (f i).lift' g :=
  lift_iInf_of_map_univ (fun s t => by simp only [inf_principal, comp, hg])
    (by rw [Function.comp_apply, hg', principal_univ])

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤

Tactic:
rw [Function.comp_apply, hg', principal_univ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
simp only [inf_principal, comp, hg]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
lemma aeval_natDegree_le {R : Type*} [CommSemiring R] {m n : ℕ}
    (F : MvPolynomial σ R) (hF : F.totalDegree ≤ m)
    (f : σ → Polynomial R) (hf : ∀ i, (f i).natDegree ≤ n) :
    (MvPolynomial.aeval f F).natDegree ≤ m * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, d i ≤ F.totalDegree

Tactic:
rw [MvPolynomial.totalDegree]

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, d i ≤ F.support.sup fun s => s.sum fun x e => e

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (∑ i ∈ d.support, d i) * n ≤ m * n

Tactic:
apply mul_le_mul' (.trans _ hF) le_rfl

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, d i ≤ F.totalDegree

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ ((aeval f) F).natDegree ≤ m * n

Tactic:
rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ (Finsupp.sum F fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e).natDegree ≤ m * n
-- Mathlib/Data/Real/EReal.lean
lemma mul_le_of_forall_lt_of_nonneg (ha : 0 ≤ a) (hc : 0 ≤ c)
    (h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c) : a * b ≤ c

Proof state:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
⊢ d ≤ c

Tactic:
rcases lt_or_le d 0 with d0 | d0

Result:
case inl
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c

case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
⊢ d ≤ c

Proof state:
case inl
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c

Tactic:
exact d0.le.trans hc

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab✝¹ : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ico 0 a
dab✝ : d < a' * b
b' : EReal
bb' : b' ∈ Ico 0 b
dab : d < a' * b'
⊢ d ≤ c

Tactic:
exact dab.le.trans (h a' aa' b' bb')

Result:
no goals

Proof state:
case inr.intro.intro
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab✝ : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ico 0 a
dab : d < a' * b
⊢ d ≤ c

Tactic:
obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1 d0 dab

Result:
case inr.intro.intro.intro.intro
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab✝¹ : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ico 0 a
dab✝ : d < a' * b
b' : EReal
bb' : b' ∈ Ico 0 b
dab : d < a' * b'
⊢ d ≤ c

Proof state:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
⊢ d ≤ c

Tactic:
obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab

Result:
case inr.intro.intro
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab✝ : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ico 0 a
dab : d < a' * b
⊢ d ≤ c

Proof state:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_

Result:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ico 0 a, ∀ b' ∈ Ico 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
⊢ d ≤ c
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sq : cosh x ^ 2 = sinh x ^ 2 + 1

Proof state:
x : ℂ
⊢ cosh x ^ 2 = sinh x ^ 2 + (cosh x ^ 2 - sinh x ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
rw [← cosh_sq_sub_sinh_sq x]

Result:
x : ℂ
⊢ cosh x ^ 2 = sinh x ^ 2 + (cosh x ^ 2 - sinh x ^ 2)
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem div (q r : ℚ) : padicNorm p (q / r) = padicNorm p q / padicNorm p r :=
  if hr : r = 0 then by simp [hr]
  else eq_div_of_mul_eq (padicNorm.nonzero hr) (by rw [← padicNorm.mul, div_mul_cancel₀ _ hr])

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q

Tactic:
rw [← padicNorm.mul, div_mul_cancel₀ _ hr]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : r = 0
⊢ padicNorm p (q / r) = padicNorm p q / padicNorm p r

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem isZero_zero [HasZeroObject V] : IsZero (zero : HomologicalComplex V c)

Proof state:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
⊢ IsZero zero

Tactic:
refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩

Result:
case refine_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default

case refine_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default

Proof state:
case refine_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default

Tactic:
ext

Result:
case refine_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ f.f i✝ = default.f i✝

Proof state:
case refine_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ f.f i✝ = Hom.f 0 i✝

Tactic:
subsingleton

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default

case refine_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default

Tactic:
all_goals
  ext
  dsimp only [zero]
  subsingleton

Result:
no goals

Proof state:
case refine_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ f.f i✝ = default.f i✝

Tactic:
dsimp only [zero]

Result:
case refine_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ f.f i✝ = Hom.f 0 i✝
-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem Pullback.continuous_totalSpaceMk [∀ x, TopologicalSpace (E x)] [FiberBundle F E]
    {f : B' → B} {x : B'} : Continuous (@TotalSpace.mk _ F (f *ᵖ E) x)

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ instTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { proj := x, snd := x_1 }) inst✝⁴

Tactic:
exact (FiberBundle.totalSpaceMk_isInducing F E (f x)).eq_induced.le

Result:
no goals

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ Continuous (TotalSpace.mk x)

Tactic:
simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose,
  induced_inf, Function.comp_def, induced_const, top_inf_eq, pullbackTopology_def]

Result:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ instTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { proj := x, snd := x_1 }) inst✝⁴
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem IsGLB.biUnion_Ioi_eq (h : IsGLB s a) : ⋃ x ∈ s, Ioi x = Ioi a

Proof state:
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
⊢ ⋃ x ∈ s, Ioi x = Ioi a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Result:
case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a

case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ioi i

Proof state:
case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a

Tactic:
exact Ioi_subset_Ioi (h.1 hx)

Result:
no goals

Proof state:
case refine_2.intro.intro.intro
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ioi i

Tactic:
exact mem_biUnion hys hyx

Result:
no goals

Proof state:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ioi i

Tactic:
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩

Result:
case refine_2.intro.intro.intro
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ioi i
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma nsmul_eq_mul (n : ℕ) (x : EReal) : n • x = n * x

Proof state:
case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ (n + 1) • x = ↑(n + 1) * x

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ]

Result:
case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ ↑n * x + x = (↑n + 1) * x

Proof state:
n : ℕ
x : EReal
⊢ n • x = ↑n * x

Tactic:
induction n with
| zero => rw [zero_smul, Nat.cast_zero, zero_mul]
| succ n ih =>
  rw [succ_nsmul, ih, Nat.cast_succ]
  convert (EReal.right_distrib_of_nonneg _ _).symm <;> simp

Result:
no goals

Proof state:
case zero
x : EReal
⊢ 0 • x = ↑0 * x

Tactic:
rw [zero_smul, Nat.cast_zero, zero_mul]

Result:
no goals

Proof state:
case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ ↑n * x + x = (↑n + 1) * x

Tactic:
convert (EReal.right_distrib_of_nonneg _ _).symm <;> simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.continuous [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) :
    Continuous T

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (T (u k) - T x) (y - T x) = inner (u k - x) (T (y - T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds 0)

Tactic:
rw [← sub_self x]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (T (u k) - T x) (y - T x) = inner (u k - x) (T (y - T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds (x - x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem find?_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.find? f).map Subtype.val = l.unattach.find? g

Proof state:
case nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (find? f []) = find? g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (find? f l) = find? g l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (find? f l) = find? g (map (fun x => x.val) l)

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : Option.map Subtype.val (find? f l) = find? g (map (fun x => x.val) l)
⊢ Option.map Subtype.val (find? f (a :: l)) = find? g (map (fun x => x.val) (a :: l))

Tactic:
simp [hf, find?_cons]

Result:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : Option.map Subtype.val (find? f l) = find? g (map (fun x => x.val) l)
⊢ Option.map Subtype.val
      (match g a.val with
      | true => some a
      | false => find? f l) =
    match g a.val with
    | true => some a.val
    | false => find? g l.unattach

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (find? f l) = find? g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp [hf, find?_cons]
  split <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : Option.map Subtype.val (find? f l) = find? g (map (fun x => x.val) l)
⊢ Option.map Subtype.val
      (match g a.val with
      | true => some a
      | false => find? f l) =
    match g a.val with
    | true => some a.val
    | false => find? g l.unattach

Tactic:
split <;> simp [ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_some' {o : Option α} : o.or (some a) = o.getD a

Proof state:
α : Type u_1
a : α
o : Option α
⊢ o.or (some a) = some (o.getD a)

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
lemma toFinite_eq_self [IsProbabilityMeasure μ] : μ.toFinite = μ

Proof state:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toFinite = μ

Tactic:
rw [Measure.toFinite, Measure.toFiniteAux, if_pos, ProbabilityTheory.cond_univ]

Result:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ IsFiniteMeasure μ