harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem mapForget_eq {X Y : T} (f : X ⟶ Y) :
    (map f) ⋙ (forget X) = (forget Y)

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X_1 : Under Y), (map f ⋙ forget X).obj X_1 = (forget Y).obj X_1

Tactic:
dsimp [Under, Under.map]

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X : StructuredArrow Y (𝟭 T)), X.right = X.right

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X : StructuredArrow Y (𝟭 T)), X.right = X.right

Tactic:
intro x

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x : StructuredArrow Y (𝟭 T)
⊢ x.right = x.right

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ map f ⋙ forget X = forget Y

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X_1 : Under Y), (map f ⋙ forget X).obj X_1 = (forget Y).obj X_1

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ autoParam
    (∀ (X_1 Y_1 : Under Y) (f_1 : X_1 ⟶ Y_1), (map f ⋙ forget X).map f_1 = eqToHom ⋯ ≫ (forget Y).map f_1 ≫ eqToHom ⋯)
    _auto✝

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x y : Under Y
u : x ⟶ y
⊢ (map f ⋙ forget X).map u = eqToHom ⋯ ≫ (forget Y).map u ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ autoParam
    (∀ (X_1 Y_1 : Under Y) (f_1 : X_1 ⟶ Y_1), (map f ⋙ forget X).map f_1 = eqToHom ⋯ ≫ (forget Y).map f_1 ≫ eqToHom ⋯)
    _auto✝

Tactic:
intros x y u

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x y : Under Y
u : x ⟶ y
⊢ (map f ⋙ forget X).map u = eqToHom ⋯ ≫ (forget Y).map u ≫ eqToHom ⋯

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x : StructuredArrow Y (𝟭 T)
⊢ x.right = x.right

Tactic:
exact rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem coe_eq_univ {H : Subgroup G} : (H : Set G) = Set.univ ↔ H = ⊤ :=
  (SetLike.ext'_iff.trans (by rfl)).symm

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ↑H = ↑⊤ ↔ ↑H = Set.univ

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/IndicatorConstPointwise.lean
lemma tendsto_indicator_const_iff_tendsto_pi_pure [T1Space β] (b : β) [NeZero b] :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
      ↔ (Tendsto As L <| Filter.pi (pure <| · ∈ A))

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔
    Tendsto As L (pi fun x => pure (x ∈ A))

Tactic:
rw [tendsto_indicator_const_iff_forall_eventually _ b, tendsto_pi]

Result:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x => As x i) L (pure (i ∈ A))

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x => As x i) L (pure (i ∈ A))

Tactic:
simp_rw [tendsto_pure]

Result:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, As x i = (i ∈ A)

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, As x i = (i ∈ A)

Tactic:
aesop

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
    δ i.castSucc ≫ σ i = 𝟙 (mk n)

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk n)

Tactic:
apply CategoryTheory.Quotient.sound

Result:
case h
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i)) (𝟙 (mk n).as)

Proof state:
case h
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i)) (𝟙 (mk n).as)

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_self

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem innerSL_apply_norm (x : E) : ‖innerSL 𝕜 x‖ = ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

Tactic:
rcases (norm_nonneg x).eq_or_gt with (h | h)

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : ‖x‖ = 0
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

Tactic:
refine (mul_le_mul_right h).mp ?_

Result:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ * ‖x‖ ≤ ‖(innerSL 𝕜) x‖ * ‖x‖

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ * ‖x‖ ≤ ‖(innerSL 𝕜) x‖ * ‖x‖

Tactic:
calc
  ‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
    rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
  _ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ‖(innerSL 𝕜) x‖ = ‖x‖

Tactic:
refine
  le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫_𝕜‖

Tactic:
rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : ‖x‖ = 0
⊢ ‖x‖ ≤ ‖(innerSL 𝕜) x‖

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ico_right (f : ∀ i, α i) (i : ι) (b : α i) :
    update f i '' Ico (f i) b = Ico f (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ico (f i) b = Ico f (update f i b)

Tactic:
simpa using image_update_Ico f i (f i) b

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
protected lemma conjExponent (hp : 1 ≤ p) : p.IsConjExponent (conjExponent p)

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ AddLECancellable p⁻¹

Tactic:
simpa

Result:
no goals

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ + p⁻¹ = 1

Tactic:
refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (by simpa) (by simpa)).1 ?_

Result:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ = 1 - p⁻¹

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ p.IsConjExponent p.conjExponent

Tactic:
rw [isConjExponent_iff, conjExponent, add_comm]

Result:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ + p⁻¹ = 1

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ = 1 - p⁻¹

Tactic:
rw [inv_eq_iff_eq_inv]

Result:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ 1 + (p - 1)⁻¹ = (1 - p⁻¹)⁻¹

Proof state:
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ⊤
⊢ 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)

Tactic:
rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]

Result:
no goals

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ p⁻¹ ≤ 1

Tactic:
simpa

Result:
no goals

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ 1 + (p - 1)⁻¹ = (1 - p⁻¹)⁻¹

Tactic:
obtain rfl | hp₁ := hp.eq_or_lt

Result:
case inl
hp : 1 ≤ 1
this : 1 ≠ 0
⊢ 1 + (1 - 1)⁻¹ = (1 - 1⁻¹)⁻¹

case inr
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1 - p⁻¹)⁻¹

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.IsConjExponent p.conjExponent

Tactic:
have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'

Result:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ p.IsConjExponent p.conjExponent

Proof state:
case inr.inr
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ⊤
⊢ 1 + (p - 1)⁻¹ = (1 - p⁻¹)⁻¹

Tactic:
calc
  1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
    rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
  _ = (1 - p⁻¹)⁻¹ := by
    rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
      ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]

Result:
no goals

Proof state:
case inr.inl
hp : 1 ≤ ⊤
this : ⊤ ≠ 0
hp₁ : 1 < ⊤
⊢ 1 + (⊤ - 1)⁻¹ = (1 - ⊤⁻¹)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case inr
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1 - p⁻¹)⁻¹

Tactic:
obtain rfl | hp := eq_or_ne p ∞

Result:
case inr.inl
hp : 1 ≤ ⊤
this : ⊤ ≠ 0
hp₁ : 1 < ⊤
⊢ 1 + (⊤ - 1)⁻¹ = (1 - ⊤⁻¹)⁻¹

case inr.inr
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ⊤
⊢ 1 + (p - 1)⁻¹ = (1 - p⁻¹)⁻¹

Proof state:
case inl
hp : 1 ≤ 1
this : 1 ≠ 0
⊢ 1 + (1 - 1)⁻¹ = (1 - 1⁻¹)⁻¹

Tactic:
simp [tsub_eq_zero_of_le]

Result:
no goals

Proof state:
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ⊤
⊢ (p - 1 + 1) / (p - 1) = (1 - p⁻¹)⁻¹

Tactic:
rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
  ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isClosed_iff_of_mem (h : ∞ ∈ s) : IsClosed s ↔ IsClosed ((↑) ⁻¹' s : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)

Tactic:
have : ∞ ∉ sᶜ := fun H => H h

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_of_not_mem this, ← isOpen_compl_iff, preimage_compl]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsEulerian.mem_edges_iff {u v : V} {p : G.Walk u v} (h : p.IsEulerian) {e : Sym2 V} :
    e ∈ p.edges ↔ e ∈ G.edgeSet :=
  ⟨ fun h => p.edges_subset_edgeSet h
  , fun he => by simpa [Nat.succ_le] using (h e he).ge ⟩

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ G.edgeSet
⊢ e ∈ p.edges

Tactic:
simpa [Nat.succ_le] using (h e he).ge

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.of_finite {s : L.Substructure M} [h : Finite s] : s.FG :=
  ⟨Set.Finite.toFinset h, by simp only [Finite.coe_toFinset, closure_eq]⟩

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
s : L.Substructure M
h : Finite ↥s
⊢ (closure L).toFun ↑(Finite.toFinset h) = s

Tactic:
simp only [Finite.coe_toFinset, closure_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem divByMonic_zero (p : R[X]) : p /ₘ 0 = 0 :=
  letI := Classical.decEq R
  if h : Monic (0 : R[X]) then by
    haveI := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]
  else by unfold divByMonic divModByMonicAux; rw [dif_neg h]

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p /ₘ 0 = 0

Tactic:
unfold divByMonic divModByMonicAux

Result:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          let_fun _wf := ⋯;
          let dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p /ₘ 0 = 0

Tactic:
haveI := monic_zero_iff_subsingleton.mp h

Result:
R : Type u
inst✝ : Ring R
p : R[X]
this✝ : DecidableEq R := Classical.decEq R
h : Monic 0
this : Subsingleton R
⊢ p /ₘ 0 = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          let_fun _wf := ⋯;
          let dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0

Tactic:
rw [dif_neg h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this✝ : DecidableEq R := Classical.decEq R
h : Monic 0
this : Subsingleton R
⊢ p /ₘ 0 = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
lemma add_def (q r : ℚ≥0) : q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

Proof state:
case a
q r : ℚ≥0
⊢ ↑(q + r) = ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den))

Tactic:
simp [Rat.add_def', Rat.mkRat_eq_divInt, num_coe, den_coe]

Result:
no goals

Proof state:
q r : ℚ≥0
⊢ q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

Tactic:
ext

Result:
case a
q r : ℚ≥0
⊢ ↑(q + r) = ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den))
-- Mathlib/Data/Multiset/Basic.lean
theorem length_toList (s : Multiset α) : s.toList.length = card s

Proof state:
α : Type u_1
s : Multiset α
⊢ s.toList.length = s.card

Tactic:
rw [← coe_card, coe_toList]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem addOrderOf_coe_rat {q : ℚ} : addOrderOf (↑(↑q * p) : AddCircle p) = q.den

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ¬q.den = 0

Tactic:
exact q.pos.ne.symm

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ↑↑q.den ≠ 0

Tactic:
norm_cast

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ¬q.den = 0

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ addOrderOf ↑(↑q * p) = q.den

Tactic:
have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
  norm_cast
  exact q.pos.ne.symm

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q * p) = q.den

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q * p) = q.den

Tactic:
rw [← q.num_divInt_den, Rat.cast_divInt_of_ne_zero _ this, Int.cast_natCast, Rat.num_divInt_den,
  addOrderOf_div_of_gcd_eq_one' q.pos q.reduced]

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_zero_iff :
    StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ 1

Tactic:
rw [← hab]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ a + b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ a + b

Tactic:
exact le_add_of_nonneg_left ha

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • 0 + b • x ∈ s

Tactic:
rw [smul_zero, zero_add]

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b • x ∈ s

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b • x ∈ s

Tactic:
exact h hb (by rw [← hab]; exact le_add_of_nonneg_left ha)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
⊢ StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

Tactic:
refine
  forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • 0 + b • x ∈ s
a : 𝕜
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • x ∈ s

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • 0 + b • x ∈ s

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • 0 + b • x ∈ s
a : 𝕜
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • x ∈ s

Tactic:
simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
  h (sub_nonneg_of_le ha₁) ha₀

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iInf₂_iff {f : ∀ i, κ i → LowerSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∀ i j, a ∈ f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → LowerSet α
⊢ a ∈ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

Tactic:
simp_rw [mem_iInf_iff]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem eq_of_factorization_eq {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : ∀ p : ℕ, a.factorization p = b.factorization p) : a = b :=
  eq_of_perm_primeFactorsList ha hb
    (by simpa only [List.perm_iff_count, primeFactorsList_count_eq] using h)

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), a.factorization p = b.factorization p
⊢ a.primeFactorsList ~ b.primeFactorsList

Tactic:
simpa only [List.perm_iff_count, primeFactorsList_count_eq] using h

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma sInf_eq_zero : sInf s = 0 ↔ 0 ∈ s

Proof state:
s : Set ℕ∞
⊢ sInf s = 0 ↔ 0 ∈ s

Tactic:
rw [← lt_one_iff_eq_zero]

Result:
s : Set ℕ∞
⊢ sInf s < 1 ↔ 0 ∈ s

Proof state:
s : Set ℕ∞
⊢ sInf s < 1 ↔ 0 ∈ s

Tactic:
simp only [sInf_lt_iff, lt_one_iff_eq_zero, exists_eq_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem isUnit_iff_degree_eq_zero : IsUnit p ↔ degree p = 0 :=
  ⟨degree_eq_zero_of_isUnit, fun h =>
    have : degree p ≤ 0

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : (C 0).degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False

Tactic:
simp only [map_zero] at h

Result:
R : Type u
inst✝ : Field R
p : R[X]
this : p.degree ≤ 0
hc : p.coeff 0 = 0
h : degree 0 = 0
⊢ False

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False

Tactic:
rw [eq_C_of_degree_le_zero this, hc] at h

Result:
R : Type u
inst✝ : Field R
p : R[X]
h : (C 0).degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
⊢ p.degree ≤ 0

Tactic:
simp [*, le_refl]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = p * C (p.coeff 0)⁻¹

Tactic:
conv in p => rw [eq_C_of_degree_le_zero this]

Result:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C (p.coeff 0) * C (p.coeff 0)⁻¹

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C (p.coeff 0) * C (p.coeff 0)⁻¹

Tactic:
rw [← C_mul, mul_inv_cancel₀ hc, C_1]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
this : p.degree ≤ 0
hc : p.coeff 0 = 0
h : degree 0 = 0
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_zero : exp 0 = 1

Proof state:
⊢ rexp 0 = 1

Tactic:
simp [Real.exp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_add_of_nonneg {x : ℝ≥0∞} (y z : ℝ) (hy : 0 ≤ y) (hz : 0 ≤ z) :
    x ^ (y + z) = x ^ y * x ^ z

Proof state:
case top
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

Tactic:
rcases hy.eq_or_lt with rfl|hy

Result:
case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ⊤ ^ (0 + z) = ⊤ ^ 0 * ⊤ ^ z

case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

Proof state:
case coe
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
x✝ : ℝ≥0
⊢ ↑x✝ ^ (y + z) = ↑x✝ ^ y * ↑x✝ ^ z

Tactic:
simp [← coe_rpow_of_nonneg, hy, hz, add_nonneg hy hz, NNReal.rpow_add_of_nonneg _ hy hz]

Result:
no goals

Proof state:
case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

Tactic:
rcases hz.eq_or_lt with rfl|hz

Result:
case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ⊤ ^ (y + 0) = ⊤ ^ y * ⊤ ^ 0

case top.inr.inr
y z : ℝ
hy✝ : 0 ≤ y
hz✝ : 0 ≤ z
hy : 0 < y
hz : 0 < z
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

Proof state:
case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ⊤ ^ (y + 0) = ⊤ ^ y * ⊤ ^ 0

Tactic:
rw [rpow_zero, mul_one, add_zero]

Result:
no goals

Proof state:
case top.inr.inr
y z : ℝ
hy✝ : 0 ≤ y
hz✝ : 0 ≤ z
hy : 0 < y
hz : 0 < z
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

Tactic:
simp [top_rpow_of_pos, hy, hz, add_pos hy hz]

Result:
no goals

Proof state:
x : ℝ≥0∞
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
induction x using recTopCoe

Result:
case top
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ⊤ ^ (y + z) = ⊤ ^ y * ⊤ ^ z

case coe
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
x✝ : ℝ≥0
⊢ ↑x✝ ^ (y + z) = ↑x✝ ^ y * ↑x✝ ^ z

Proof state:
case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ⊤ ^ (0 + z) = ⊤ ^ 0 * ⊤ ^ z

Tactic:
rw [rpow_zero, one_mul, zero_add]

Result:
no goals
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a:α) = b)
    (H : (a' - b')^n - (a - b) = 0) : a' = b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Result:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ a' - b' = 0

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ a' - b' = 0

Tactic:
apply pow_eq_zero (n := n)

Result:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ (a' - b') ^ n = 0

Proof state:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ (a' - b') ^ n = 0

Tactic:
rwa [sub_eq_zero, p] at H

Result:
no goals