harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem IsGLB.biUnion_Ici_eq_Ioi (a_glb : IsGLB s a) (a_not_mem : a ∉ s) :
    ⋃ x ∈ s, Ici x = Ioi a

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

Tactic:
rw [mem_iUnion₂]

Result:
case refine_2.intro.intro.intro
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_not_mem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ ∃ i, ∃ (_ : i ∈ s), x ∈ Ici i

Proof state:
case refine_2.intro.intro.intro
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_not_mem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ ∃ i, ∃ (_ : i ∈ s), x ∈ Ici i

Tactic:
exact ⟨y, hys, hyx.le⟩

Result:
no goals

Proof state:
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_not_mem : a ∉ s
⊢ ⋃ x ∈ s, Ici 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 : α
a_glb : IsGLB s a
a_not_mem : a ∉ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ioi a

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

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

Tactic:
exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_not_mem) hx)

Result:
no goals

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

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

Result:
case refine_2.intro.intro.intro
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_not_mem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ici i
-- Mathlib/Data/Nat/Init.lean
lemma mul_lt_mul'' (hac : a < c) (hbd : b < d) : a * b < c * d :=
  Nat.mul_lt_mul_of_lt_of_le hac (Nat.le_of_lt hbd) <| by omega

Proof state:
a b c d : ℕ
hac : a < c
hbd : b < d
⊢ 0 < d

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_erase_self [LawfulBEq α] (h : m.1.WF) {k : α} : (m.erase k).get? k = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
⊢ (m.erase k).get? k = none

Tactic:
simp_to_model [erase] using List.getValueCast?_eraseKey_self

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem card_eq_pow_finrank [Fintype V] : Fintype.card V = q ^ Module.finrank K V

Proof state:
K : Type u_1
V : Type u_3
inst✝⁴ : Fintype K
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Fintype V
⊢ Fintype.card V = q ^ Module.finrank K V

Tactic:
let b := IsNoetherian.finsetBasis K V

Result:
K : Type u_1
V : Type u_3
inst✝⁴ : Fintype K
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Fintype V
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K V } K V := IsNoetherian.finsetBasis K V
⊢ Fintype.card V = q ^ Module.finrank K V

Proof state:
K : Type u_1
V : Type u_3
inst✝⁴ : Fintype K
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Fintype V
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K V } K V := IsNoetherian.finsetBasis K V
⊢ Fintype.card V = q ^ Module.finrank K V

Tactic:
rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem gradedMonoid_eq_of_cast {a b : GradedMonoid fun n => ⨂[R] _ : Fin n, M} (h : a.fst = b.fst)
    (h2 : cast R M h a.snd = b.snd) : a = b

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ a = b

Tactic:
refine gradedMonoid_eq_of_reindex_cast h ?_

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ (reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (reindex R (fun x => M) (finCongr h)) a.snd = b.snd
⊢ (reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd

Tactic:
rw [← finCongr_eq_equivCast, ← h2]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ (reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd

Tactic:
rw [cast] at h2

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (reindex R (fun x => M) (finCongr h)) a.snd = b.snd
⊢ (reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd
-- Mathlib/Data/Sign.lean
theorem neg_iff {a : SignType} : a < 0 ↔ a = -1

Proof state:
a : SignType
⊢ a < 0 ↔ a = -1

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma InjOn.image_subset_image_iff (h : s.InjOn f) (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) :
    f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂

Proof state:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂

Tactic:
refine ⟨fun h' ↦ ?_, image_subset _⟩

Result:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ s₁ ⊆ s₂

Proof state:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ s₁ ⊆ s₂

Tactic:
rw [← h.preimage_image_inter h₁, ← h.preimage_image_inter h₂]

Result:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' (f '' s₁) ∩ s ⊆ f ⁻¹' (f '' s₂) ∩ s

Proof state:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' (f '' s₁) ∩ s ⊆ f ⁻¹' (f '' s₂) ∩ s

Tactic:
exact inter_subset_inter_left _ (preimage_mono h')

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toArray_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l, P x} :
   (l.attachWith P H).toArray = l.toArray.attachWith P (by simpa using H)

Proof state:
α : Type u_1
n : Nat
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l → P x
⊢ (l.attachWith P H).toArray = l.attachWith P ⋯

Tactic:
simp [attachWith]

Result:
no goals

Proof state:
α : Type ?u.3599
n : Nat
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l → P x
⊢ ∀ (x : α), x ∈ l.toArray → P x

Tactic:
simpa using H

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_lintegral (f : α →ₛ ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
    (restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (f ⁻¹' {r} ∩ s) :=
  calc
    (restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (restrict f s ⁻¹' {r}) :=
      lintegral_eq_of_subset _ fun x hx =>
        if hxs : x ∈ s then fun _ => by
          simp only [f.restrict_apply hs, indicator_of_mem hxs, mem_range_self]
        else False.elim <| hx <| by simp [*]
    _ = ∑ r ∈ f.range, r * μ (f ⁻¹' {r} ∩ s) :=
      Finset.sum_congr rfl <|
        forall_mem_range.2 fun b =>
          if hb : f b = 0 then by simp only [hb, zero_mul]
          else by rw [restrict_preimage_singleton _ hs hb, inter_comm]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : (f.restrict s) x ≠ 0
hxs : x ∈ s
x✝ : μ (⇑(f.restrict s) ⁻¹' {(f.restrict s) x}) ≠ 0
⊢ (f.restrict s) x ∈ f.range

Tactic:
simp only [f.restrict_apply hs, indicator_of_mem hxs, mem_range_self]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬f b = 0
⊢ f b * μ (⇑(f.restrict s) ⁻¹' {f b}) = f b * μ (⇑f ⁻¹' {f b} ∩ s)

Tactic:
rw [restrict_preimage_singleton _ hs hb, inter_comm]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : f b = 0
⊢ f b * μ (⇑(f.restrict s) ⁻¹' {f b}) = f b * μ (⇑f ⁻¹' {f b} ∩ s)

Tactic:
simp only [hb, zero_mul]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : (f.restrict s) x ≠ 0
hxs : x ∉ s
⊢ (f.restrict s) x = 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem doset_eq_of_mem {H K : Subgroup G} {a b : G} (hb : b ∈ doset a H K) :
    doset b H K = doset a H K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
hb : b ∈ doset a ↑H ↑K
⊢ doset b ↑H ↑K = doset a ↑H ↑K

Tactic:
obtain ⟨h, hh, k, hk, rfl⟩ := mem_doset.1 hb

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doset a ↑H ↑K
⊢ doset (h * a * k) ↑H ↑K = doset a ↑H ↑K

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doset a ↑H ↑K
⊢ doset (h * a * k) ↑H ↑K = doset a ↑H ↑K

Tactic:
rw [doset, doset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton, mul_assoc,
  mul_assoc, Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc,
  Subgroup.subgroup_mul_singleton hh]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_insertList_of_mem [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert) :
    getValueCastD k' (insertList l toInsert) fallback =
    cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ k = k'

Tactic:
exact LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
⊢ getValueCastD k' (insertList l toInsert) fallback = cast ⋯ v

Tactic:
rw [getValueCastD_eq_getValueCast?,
  getValueCast?_insertList_of_mem k_beq distinct_l distinct_toInsert mem, Option.getD_some]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_mul_cos_pow_odd (m n : ℕ) :
    (∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1)) = ∫ u in sin a..sin b, u^m * (↑1 - u ^ 2) ^ n :=
  have hc : Continuous fun u : ℝ => u ^ m * (↑1 - u ^ 2) ^ n

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * ((cos x * cos x) ^ n * cos x) =
    ∫ (x : ℝ) in a..b, sin x ^ m * ((1 - sin x * sin x) ^ n * cos x)

Tactic:
congr! 5

Result:
case h.e'_4.h.h.e'_6.h.e'_5.h.e'_5
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ * cos x✝ = 1 - sin x✝ * sin x✝

Proof state:
a b : ℝ
m n : ℕ
⊢ Continuous fun u => u ^ m * (1 - u ^ 2) ^ n

Tactic:
fun_prop

Result:
no goals

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x = ∫ (u : ℝ) in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n

Tactic:
exact integral_comp_mul_deriv (fun x _ => hasDerivAt_sin x) continuousOn_cos hc

Result:
no goals

Proof state:
case h.e'_4.h.h.e'_6.h.e'_5.h.e'_5
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ * cos x✝ = 1 - sin x✝ * sin x✝

Tactic:
rw [← sq, ← sq, cos_sq']

Result:
no goals

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x

Tactic:
simp only [_root_.pow_zero, _root_.pow_succ, mul_assoc, pow_mul, one_mul]

Result:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * ((cos x * cos x) ^ n * cos x) =
    ∫ (x : ℝ) in a..b, sin x ^ m * ((1 - sin x * sin x) ^ n * cos x)
-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem hom_antipode {A B : Hopf_ C} (f : A ⟶ B) :
    f.hom.hom ≫ B.antipode = A.antipode ≫ f.hom.hom

Proof state:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ ((f.hom.hom ≫ B.X.comul.hom) ≫ B.antipode ▷ B.X.X.X) ≫ B.X.X.mul = A.X.counit.hom ≫ B.X.X.one

Tactic:
slice_lhs 2 4 =>
  rw [B.antipode_left]

Result:
case hba
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Hopf_ C
f : A ⟶ B
⊢ f.hom.hom ≫ B.X.counit.hom ≫ B.X.X.one = A.X.counit.hom ≫ B.X.X.one
-- Mathlib/RingTheory/Int/Basic.lean
theorem Int.Prime.dvd_mul {m n : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ m * n) :
    p ∣ m.natAbs ∨ p ∣ n.natAbs

Proof state:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.natCast_dvd]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/WithAbs.lean
theorem extensionEmbedding_of_comp_coe (h : ∀ x, ‖f x‖ = v x) (x : K) :
    extensionEmbedding_of_comp h x = f x

Proof state:
K : Type u_3
inst✝² : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝¹ : NormedField L
inst✝ : CompleteSpace L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x : K
⊢ (extensionEmbedding_of_comp h) ↑x = f x

Tactic:
rw [← UniformSpace.Completion.extensionHom_coe f
  (WithAbs.isUniformInducing_of_comp h).uniformContinuous.continuous]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem dist_div_sin_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : dist p₁ p₂ / Real.Angle.sin (∡ p₂ 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
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  dist_div_sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inl (left_ne_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₁).sign = 1

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

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)
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = 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
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
-- Mathlib/Data/Complex/Norm.lean
theorem norm_le_sqrt_two_mul_max (z : ℂ) : ‖z‖ ≤ Real.sqrt 2 * max |z.re| |z.im|

Proof state:
case pos
x y : ℝ
hle : |x| ≤ |y|
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Tactic:
calc
  Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt (y ^ 2 + y ^ 2) :=
    Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
  _ = Real.sqrt 2 * max |x| |y| := by
    rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]

Result:
no goals

Proof state:
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ √(x ^ 2 + x ^ 2) = √2 * (|x| ⊔ |y|)

Tactic:
rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]

Result:
no goals

Proof state:
case mk
x y : ℝ
⊢ ‖{ re := x, im := y }‖ ≤ √2 * (|{ re := x, im := y }.re| ⊔ |{ re := x, im := y }.im|)

Tactic:
simp only [norm_def, normSq_mk, norm_def, ← sq]

Result:
case mk
x y : ℝ
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Proof state:
x y : ℝ
hle : |x| ≤ |y|
⊢ √(y ^ 2 + y ^ 2) = √2 * (|x| ⊔ |y|)

Tactic:
rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]

Result:
no goals

Proof state:
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Tactic:
have hle' := le_of_not_le hle

Result:
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Proof state:
case mk
x y : ℝ
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Tactic:
by_cases hle : |x| ≤ |y|

Result:
case pos
x y : ℝ
hle : |x| ≤ |y|
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

case neg
x y : ℝ
hle : ¬|x| ≤ |y|
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Proof state:
z : ℂ
⊢ ‖z‖ ≤ √2 * (|z.re| ⊔ |z.im|)

Tactic:
obtain ⟨x, y⟩ := z

Result:
case mk
x y : ℝ
⊢ ‖{ re := x, im := y }‖ ≤ √2 * (|{ re := x, im := y }.re| ⊔ |{ re := x, im := y }.im|)

Proof state:
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * (|x| ⊔ |y|)

Tactic:
rw [add_comm]

Result:
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ √(y ^ 2 + x ^ 2) ≤ √2 * (|x| ⊔ |y|)

Proof state:
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ √(y ^ 2 + x ^ 2) ≤ √2 * (|x| ⊔ |y|)

Tactic:
calc
  Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt (x ^ 2 + x ^ 2) :=
    Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle') _)
  _ = Real.sqrt 2 * max |x| |y| := by
    rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem dvd_iff_mod_eq_zero {m n : Num} : m ∣ n ↔ n % m = 0

Proof state:
m n : Num
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_nat, Nat.dvd_iff_mod_eq_zero, ← to_nat_inj, mod_to_nat]

Result:
m n : Num
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0

Proof state:
m n : Num
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_X_pow {k : ℕ} : content ((X : R[X]) ^ k) = 1

Proof state:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
k : ℕ
hi : (X ^ k).content = 1
⊢ (X ^ (k + 1)).content = 1

Tactic:
rw [pow_succ', content_X_mul, hi]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ (X ^ 0).content = 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
k : ℕ
⊢ (X ^ k).content = 1

Tactic:
induction' k with k hi

Result:
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ (X ^ 0).content = 1

case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
k : ℕ
hi : (X ^ k).content = 1
⊢ (X ^ (k + 1)).content = 1
-- Mathlib/Analysis/NormedSpace/ENormedSpace.lean
theorem map_sub_le (x y : V) : e (x - y) ≤ e x + e y :=
  calc
    e (x - y) = e (x + -y)

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
x y : V
⊢ ↑e x + ↑e (-y) = ↑e x + ↑e y

Tactic:
rw [e.map_neg]

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (x + -y)

Tactic:
rw [sub_eq_add_neg]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem ofPrime_valuation_eq_one_iff_mem_primeCompl (A : ValuationSubring K) (P : Ideal A)
    [P.IsPrime] (x : A) : (ofPrime A P).valuation x = 1 ↔ x ∈ P.primeCompl

Proof state:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ x ∈ P.primeCompl

Tactic:
rw [← IsLocalization.AtPrime.isUnit_to_map_iff (A.ofPrime P) P x, valuation_eq_one_iff]

Result:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1

Proof state:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1

Tactic:
rfl

Result:
no goals