harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/Compact.lean
theorem image_uIcc (h : ContinuousOn f <| [[a, b]]) :
    f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
exacts [bddBelow_Icc, bddAbove_Icc]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
refine h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm

Result:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])

Tactic:
refine csInf_le_csSup ?_ ?_ (nonempty_uIcc.image _) <;> rw [h.image_uIcc_eq_Icc]

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
-- Mathlib/FieldTheory/Separable.lean
theorem IsSeparable.isIntegral {x : K} (h : IsSeparable F x) : IsIntegral F x

Proof state:
case inl
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Subsingleton F
this : Subsingleton K
⊢ IsIntegral F x

Tactic:
exact ⟨1, monic_one, Subsingleton.elim _ _⟩

Result:
no goals

Proof state:
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
⊢ IsIntegral F x

Tactic:
cases subsingleton_or_nontrivial F

Result:
case inl
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Subsingleton F
⊢ IsIntegral F x

case inr
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Nontrivial F
⊢ IsIntegral F x

Proof state:
case inl
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Subsingleton F
⊢ IsIntegral F x

Tactic:
haveI := Module.subsingleton F K

Result:
case inl
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Subsingleton F
this : Subsingleton K
⊢ IsIntegral F x
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.fiberwise_left :
    f =O[l ×ˢ l'] g → ∀ᶠ b in l', (f ⟨·, b⟩) =O[l] (g ⟨·, b⟩)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun x => f (x, b)) =O[l] fun x => g (x, b)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ (∃ c, ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}) → {b | ∃ c, {x | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}
⊢ {b | ∃ c, {x | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'

Tactic:
exact mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ (∃ c, ∃ t₁ ∈ l, ∃ t₂ ∈ l', t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}) → {b | ∃ c, {x | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'

Tactic:
rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}
⊢ {b | ∃ c, {x | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem homogeneousComponent_eq_zero (h : φ.totalDegree < n) : homogeneousComponent n φ = 0

Proof state:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e => e) < n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ d.degree ≠ n

Tactic:
exact ne_of_lt (h d hd)

Result:
no goals

Proof state:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e => e) < n
⊢ ∀ d ∈ φ.support, d.degree ≠ n

Tactic:
intro d hd

Result:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e => e) < n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ d.degree ≠ n

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ (homogeneousComponent n) φ = 0

Tactic:
apply homogeneousComponent_eq_zero'

Result:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ ∀ d ∈ φ.support, d.degree ≠ n

Proof state:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ ∀ d ∈ φ.support, d.degree ≠ n

Tactic:
rw [totalDegree, Finset.sup_lt_iff (lt_of_le_of_lt (Nat.zero_le _) h)] at h

Result:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e => e) < n
⊢ ∀ d ∈ φ.support, d.degree ≠ n
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_lcm_mul (h : Commute x y):
    orderOf y ∣ Nat.lcm (orderOf x) (orderOf (x * y))

Proof state:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
conv_lhs =>
  rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
    _root_.pow_succ, mul_assoc]

Result:
case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))

Proof state:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
rw [h0, lcm_zero_left]

Result:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0

Proof state:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
by_cases h0 : orderOf x = 0

Result:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Proof state:
case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
exact
  (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
    (lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (dvd_lcm_left _ _), dvd_lcm_right _ _⟩)

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
lemma prod {C₁ C₂ : Type*} [Category C₁] [Category C₂]
    {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂}
    {E₁ E₂ : Type*} [Category E₁] [Category E₂] {F₁ : C₁ ⥤ E₁} {F₂ : C₂ ⥤ E₂}
    (h₁ : W₁.IsInvertedBy F₁) (h₂ : W₂.IsInvertedBy F₂) :
    (W₁.prod W₂).IsInvertedBy (F₁.prod F₂) := fun _ _ f hf => by
  rw [isIso_prod_iff]
  exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_5, u_1} C₁
inst✝² : Category.{u_6, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{u_7, u_3} E₁
inst✝ : Category.{u_8, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f)

Tactic:
rw [isIso_prod_iff]

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_5, u_1} C₁
inst✝² : Category.{u_6, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{u_7, u_3} E₁
inst✝ : Category.{u_8, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{u_5, u_1} C₁
inst✝² : Category.{u_6, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{u_7, u_3} E₁
inst✝ : Category.{u_8, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2

Tactic:
exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem unitization_injective (h1 : (1 : A) ∉ s) : Function.Injective (unitization s) :=
  AlgHomClass.unitization_injective s h1 (unitization s) fun _ ↦ by simp

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
x✝ : ↥s
⊢ (unitization s) ↑x✝ = ↑x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem mulRec_zero_eq (x y : BitVec w) :
    mulRec x y 0 = if y.getLsbD 0 then x else 0

Proof state:
w : Nat
x y : BitVec w
⊢ x.mulRec y 0 = if y.getLsbD 0 = true then x else 0

Tactic:
simp [mulRec]

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem diophFn_comp {f : Vector3 ℕ n → ℕ} (df : DiophFn f) (g : Vector3 ((α → ℕ) → ℕ) n)
    (dg : VectorAllP DiophFn g) : DiophFn fun v => f fun i => g i v :=
  dioph_comp ((diophFn_vec _).1 df) ((fun v => v none)::fun i v => g i (v ∘ some)) <| by
    simp only [vectorAllP_cons]
    exact ⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i =>
          reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩

Proof state:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ (DiophFn fun v => v none) ∧ VectorAllP DiophFn fun i v => g i (v ∘ some)

Tactic:
exact ⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i =>
      reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩

Result:
no goals

Proof state:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ VectorAllP DiophFn ((fun v => v none) :: fun i v => g i (v ∘ some))

Tactic:
simp only [vectorAllP_cons]

Result:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ (DiophFn fun v => v none) ∧ VectorAllP DiophFn fun i v => g i (v ∘ some)
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_erase_lt (hp : p ≠ 0) : degree (p.erase (natDegree p)) < degree p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (p.support.erase p.natDegree).max ≠ ↑p.natDegree

Tactic:
exact fun h => not_mem_erase _ _ (mem_of_max h)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (erase p.natDegree p).degree < p.degree

Tactic:
apply lt_of_le_of_ne (degree_erase_le _ _)

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (erase p.natDegree p).degree ≠ p.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (erase p.natDegree p).degree ≠ p.degree

Tactic:
rw [degree_eq_natDegree hp, degree, support_erase]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (p.support.erase p.natDegree).max ≠ ↑p.natDegree
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_left_min {a b : Nat} : min (b + a) a = a

Proof state:
a b : Nat
⊢ min (b + a) a = a

Tactic:
rw [Nat.min_comm, min_add_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
    (hl : DistinctKeys l) (h : Perm l l') : getValueCast? a l = getValueCast? a l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getValueCast? a l = getValueCast? a l'

Tactic:
rw [getValueCast?_eq_getEntry?, getValueCast?_eq_getEntry?,
  Option.dmap_congr (getEntry?_of_perm hl h)]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem oreDiv_mul_oreDiv {r₁ : R} {r₂ : R} {s₁ s₂ : S} :
    (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
with_unfolding_all rfl

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
    (a * b).factorization = a.factorization + b.factorization

Proof state:
case h
a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ (a * b).factorization q = (a.factorization + b.factorization) q

Tactic:
rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]

Result:
no goals

Proof state:
a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
ext q

Result:
case h
a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ (a * b).factorization q = (a.factorization + b.factorization) q
-- Mathlib/Data/List/Indexes.lean
theorem new_def_eq_old_def :
    ∀ (f : ℕ → α → β) (l : List α), l.mapIdx f = List.oldMapIdx f l

Proof state:
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α), mapIdx f l = List.oldMapIdx f l

Tactic:
intro f

Result:
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α), mapIdx f l = List.oldMapIdx f l

Proof state:
case ind
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
h : mapIdx f l = List.oldMapIdx f l
⊢ mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])

Tactic:
rw [List.oldMapIdx_append, mapIdx_append_one, h]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α), mapIdx f l = List.oldMapIdx f l

Tactic:
apply list_reverse_induction

Result:
case base
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = List.oldMapIdx f []

case ind
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])

Proof state:
case base
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = List.oldMapIdx f []

Tactic:
rfl

Result:
no goals

Proof state:
case ind
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])

Tactic:
intro l e h

Result:
case ind
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
h : mapIdx f l = List.oldMapIdx f l
⊢ mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem disjoint_nhds_nhds [T2Space X] {x y : X} : Disjoint (𝓝 x) (𝓝 y) ↔ x ≠ y :=
  ⟨fun hd he => by simp [he, nhds_neBot.ne] at hd, (t2Space_iff_disjoint_nhds.mp ‹_› ·)⟩

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x y : X
hd : Disjoint (𝓝 x) (𝓝 y)
he : x = y
⊢ False

Tactic:
simp [he, nhds_neBot.ne] at hd

Result:
no goals
-- Mathlib/Logic/Nontrivial/Basic.lean
theorem nontrivial_at (i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] :
    Nontrivial (∀ i : I, f i)

Proof state:
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)

Tactic:
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

Result:
no goals

Proof state:
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)

Tactic:
letI := Classical.decEq (∀ i : I, f i)

Result:
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)
-- Mathlib/Algebra/Ring/Rat.lean
lemma mkRat_eq_div (n : ℤ) (d : ℕ) : mkRat n d = n / d

Proof state:
n : ℤ
d : ℕ
⊢ mkRat n d = ↑n / ↑d

Tactic:
simp only [mkRat_eq_divInt, divInt_eq_div, Int.cast_natCast]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.mul_const (hc : HasStrictFDerivAt c c' x) (d : 𝔸') :
    HasStrictFDerivAt (fun y => c y * d) (d • c') x

Proof state:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
z : E
⊢ (d • c') z = (c'.smulRight d) z

Tactic:
apply mul_comm

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HasStrictFDerivAt (fun y => c y * d) (d • c') x

Tactic:
convert hc.mul_const' d

Result:
case h.e'_12.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ d • c' = c'.smulRight d

Proof state:
case h.e'_12.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ d • c' = c'.smulRight d

Tactic:
ext z

Result:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
z : E
⊢ (d • c') z = (c'.smulRight d) z
-- Mathlib/Algebra/CharP/Two.lean
theorem orderOf_neg_one [Nontrivial R] : orderOf (-1 : R) = if ringChar R = 2 then 1 else 2

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ orderOf (-1) = if ringChar R = 2 then 1 else 2

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1

case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2

Proof state:
case neg.hg1
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1

Tactic:
simpa [neg_one_eq_one_iff] using h

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2

Tactic:
apply orderOf_eq_prime

Result:
case neg.hg
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

case neg.hg1
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1

Proof state:
case neg.hg
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1

Tactic:
rw [neg_one_eq_one_iff.2 h, orderOf_one]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.isBigO_symm (h : u ~[l] v) : v =O[l] u

Proof state:
case h.e'_8.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
x✝ : α
⊢ u x✝ = (u - v) x✝ + v x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
⊢ v =O[l] u

Tactic:
convert h.isLittleO.right_isBigO_add

Result:
case h.e'_8.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
h : u ~[l] v
x✝ : α
⊢ u x✝ = (u - v) x✝ + v x✝
-- Mathlib/Control/Bitraversable/Lemmas.lean
theorem tsnd_eq_snd_id {α β β'} (f : β → β') (x : t α β) :
    tsnd (F := Id) (pure ∘ f) x = pure (snd f x)

Proof state:
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
inst✝ : LawfulBitraversable t
α β β' : Type u
f : β → β'
x : t α β
⊢ tsnd (pure ∘ f) x = pure (snd f x)

Tactic:
apply bitraverse_eq_bimap_id

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_sub_left (w : ι → ℝ) (f₁ f₂ g : ∀ i, E i) :
    ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ wInner w (f₁ - f₂) g = wInner w f₁ g - wInner w f₂ g

Tactic:
simp_rw [sub_eq_add_neg, wInner_add_left, wInner_neg_left]

Result:
no goals