harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem extend_agrees {x : FamilyOfElements P R} (t : x.Compatible) {f : Y ⟶ X} (hf : R f) :
    x.sieveExtend f (le_generate R Y hf) = x f hf

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f

Tactic:
rw [id_comp]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ P.map (𝟙 Y).op (x f hf) = x f hf

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = f

Tactic:
exact h.choose_spec.choose_spec.2

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ P.map ⋯.choose.op (x ⋯.choose ⋯) = x f hf

Tactic:
rw [t h.choose (𝟙 _) _ hf _]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ P.map (𝟙 Y).op (x f hf) = x f hf

C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ x.sieveExtend f ⋯ = x f hf

Tactic:
unfold FamilyOfElements.sieveExtend

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ P.map ⋯.choose.op (x ⋯.choose ⋯) = x f hf

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
⊢ x.sieveExtend f ⋯ = x f hf

Tactic:
have h := (le_generate R Y hf).choose_spec

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ x.sieveExtend f ⋯ = x f hf
-- Mathlib/Data/ENNReal/Inv.lean
lemma iSup_mul (f : ι → ℝ≥0∞) (a : ℝ≥0∞) : (⨆ i, f i) * a = ⨆ i, f i * a

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨆ i, f i) * a = ⨆ i, f i * a

Tactic:
simp [mul_comm, mul_iSup]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem snd_map (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : snd (map f x) = f (snd x)

Proof state:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : tsze R' M
⊢ ((map f) x).snd = f x.snd

Tactic:
simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma finite_quotient_of_pretransitive_of_index_ne_zero {X : Type*} [MulAction G X]
    [MulAction.IsPretransitive G X] (hi : H.index ≠ 0) :
    Finite <| MulAction.orbitRel.Quotient H X

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
this : Subsingleton (MulAction.orbitRel.Quotient G X)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
this : Subsingleton (MulAction.orbitRel.Quotient G X)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)
-- Mathlib/Data/Complex/Norm.lean
lemma norm_add_mul_I (x y : ℝ) : ‖x + y * I‖ = (x ^ 2 + y ^ 2).sqrt

Proof state:
x y : ℝ
⊢ ‖↑x + ↑y * I‖ = √(x ^ 2 + y ^ 2)

Tactic:
rw [← normSq_add_mul_I]

Result:
x y : ℝ
⊢ ‖↑x + ↑y * I‖ = √(normSq (↑x + ↑y * I))

Proof state:
x y : ℝ
⊢ ‖↑x + ↑y * I‖ = √(normSq (↑x + ↑y * I))

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/RingHom/Injective.lean
lemma _root_.RingHom.injective_respectsIso :
    RingHom.RespectsIso (fun f ↦ Function.Injective f)

Proof state:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom

Tactic:
intro R S _ _ e

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ Function.Injective ⇑e.toRingHom

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ Function.Injective ⇑e.toRingHom

Tactic:
exact e.bijective.injective

Result:
no goals

Proof state:
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Injective ⇑f

Tactic:
apply RingHom.injective_stableUnderComposition.respectsIso

Result:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem map_zero (d : ℕ) (a : Fin 0 → ℕ) : map d a = 0

Proof state:
d : ℕ
a : Fin 0 → ℕ
⊢ (map d) a = 0

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem results_thinkN_pure (a : α) (n) : Results (thinkN (pure a) n) a n

Proof state:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
⊢ ((pure a).thinkN n).Results a n

Tactic:
rwa [Nat.zero_add] at this

Result:
no goals

Proof state:
α : Type u
a : α
n : ℕ
⊢ ((pure a).thinkN n).Results a n

Tactic:
have := results_thinkN n (results_pure a)

Result:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
⊢ ((pure a).thinkN n).Results a n
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem universalHom_commutes {r : R} : universalHom f fS hf (numeratorHom r) = f r

Proof state:
R : Type u_1
inst✝² : Semiring R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r : R
⊢ (universalHom f fS hf) (numeratorHom r) = f r

Tactic:
simp [numeratorHom_apply, universalHom_apply]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem card_divisors_mul {m n : ℕ} (hmn : m.Coprime n) :
    #(m * n).divisors = #m.divisors * #n.divisors

Proof state:
m n : ℕ
hmn : m.Coprime n
⊢ #(m * n).divisors = #m.divisors * #n.divisors

Tactic:
simp only [← sigma_zero_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Predicate.lean
@[simp]
lemma isoOfHom_id_inv (X : C) (hX : W (𝟙 X)) :
    (isoOfHom L W (𝟙 X) hX).inv = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
hX : W (𝟙 X)
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)

Tactic:
rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
  isoOfHom_hom, Functor.map_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
    (h : ∀ x ∈ l, p x) {S : β → β → Prop}
    (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
    Pairwise S (l.pmap f h)

Proof state:
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → R a b → ∀ (h₁ : p a) (h₂ : p b), S (f a h₁) (f b h₂)

Tactic:
intros

Result:
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ S (f a✝³ h₁✝) (f b✝ h₂✝)

Proof state:
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ Pairwise S (List.pmap f l h)

Tactic:
refine (pairwise_pmap h).2 (Pairwise.imp_of_mem ?_ hl)

Result:
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → R a b → ∀ (h₁ : p a) (h₂ : p b), S (f a h₁) (f b h₂)

Proof state:
case a
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ R a✝³ b✝

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ S (f a✝³ h₁✝) (f b✝ h₂✝)

Tactic:
apply hS

Result:
case a
α : Type u_1
R : α → α → Prop
β : Type u_2
l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ R a✝³ b✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffixOf_cons_nil : isSuffixOf (a::as) ([] : List α) = false

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
as : List α
⊢ (a :: as).isSuffixOf [] = false

Tactic:
simp [isSuffixOf]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `φ` are strongly cocartesian, then so is `ψ`. -/
protected lemma of_comp [IsStronglyCocartesian p f φ] [IsStronglyCocartesian p (f ≫ g) (φ ≫ ψ)]
    [IsHomLift p g ψ] : IsStronglyCocartesian p g ψ where
  universal_property'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = τ

Tactic:
have h₁ : IsHomLift p (f ≫ g ≫ h) (φ ≫ τ) := by simpa using IsHomLift.comp p f (g ≫ h) φ τ

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = τ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : p.IsHomLift (f ≫ g ≫ h) (φ ≫ τ)
⊢ φ ≫ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = φ ≫ τ

Tactic:
simp only [← assoc, fac]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem Tendsto.prod_map_prod_atTop [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ}
    {g : β → γ} (hf : Tendsto f F atTop) (hg : Tendsto g G atTop) :
    Tendsto (Prod.map f g) (F ×ˢ G) atTop

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)

Tactic:
exact hf.prod_map hg

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : Real.Angle.tan (∡ p₃ p₁ p₂) * dist p₁ p₂ = dist p₃ p₂

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

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
  tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inr (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₂).tan * dist p₁ p₂ = dist p₃ p₂

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

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma image_comap_C_basicOpen (f : MvPolynomial σ R) :
    comap (C (σ := σ)) '' basicOpen f = (zeroLocus (Set.range f.coeff))ᶜ

Proof state:
case h
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
p : PrimeSpectrum R
⊢ (∃ i, coeff i f ∉ p.asIdeal) ↔ p ∈ (zeroLocus (Set.range fun m => coeff m f))ᶜ

Tactic:
simp [Set.range_subset_iff]

Result:
no goals

Proof state:
case h
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
p : PrimeSpectrum R
⊢ p ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ p ∈ (zeroLocus (Set.range fun m => coeff m f))ᶜ

Tactic:
rw [mem_image_comap_C_basicOpen]

Result:
case h
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
p : PrimeSpectrum R
⊢ (∃ i, coeff i f ∉ p.asIdeal) ↔ p ∈ (zeroLocus (Set.range fun m => coeff m f))ᶜ

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
⊢ ⇑(comap C) '' ↑(basicOpen f) = (zeroLocus (Set.range fun m => coeff m f))ᶜ

Tactic:
ext p

Result:
case h
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
p : PrimeSpectrum R
⊢ p ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ p ∈ (zeroLocus (Set.range fun m => coeff m f))ᶜ
-- Mathlib/Topology/MetricSpace/Kuratowski.lean
theorem embeddingOfSubset_dist_le (a b : α) :
    dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b

Proof state:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b

Tactic:
convert abs_dist_sub_le a b (x n) using 2

Result:
case h.e'_3.h.e'_1
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)

Proof state:
case h.e'_3.h.e'_1
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)

Tactic:
ring

Result:
no goals

Proof state:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b

Tactic:
refine lp.norm_le_of_forall_le dist_nonneg fun n => ?_

Result:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ ‖↑(embeddingOfSubset x a - embeddingOfSubset x b) n‖ ≤ dist a b

Proof state:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ ‖↑(embeddingOfSubset x a - embeddingOfSubset x b) n‖ ≤ dist a b

Tactic:
simp only [lp.coeFn_sub, Pi.sub_apply, embeddingOfSubset_coe, Real.dist_eq]

Result:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_succ_succ (r : R) (k : ℕ) :
    multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)

Tactic:
simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]

Result:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (ascPochhammer ℕ (k + 1)).smeval (r + 1) =
    (ascPochhammer ℕ (k + 1)).smeval r + (k + 1).factorial • multichoose (r + 1) k

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]

Result:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (ascPochhammer ℕ (k + 1)).smeval (r + 1) =
    (ascPochhammer ℕ (k + 1)).smeval r + (k + 1).factorial • multichoose (r + 1) k

Tactic:
rw [add_comm (smeval (ascPochhammer ℕ (k+1)) r), ascPochhammer_succ_succ r k]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₈_int_eq_if_mod_eight (n : ℤ) :
    χ₈ n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Proof state:
n : ℤ
⊢ χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
have help :
  ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 := by
  decide

Result:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Proof state:
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1

Tactic:
decide

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
exact help (n % 8) (Int.emod_nonneg n (by omega)) (Int.emod_lt n (by omega))

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 8 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 2 ∣ 8

Tactic:
omega

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
rw [← Int.emod_emod_of_dvd n (by omega : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]

Result:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ χ₈ ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
-- Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean
theorem dist_birkhoffAverage_birkhoffAverage_le (f : α → α) (g : α → E) (n : ℕ) (x y : α) :
    dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) ≤
      (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
  (dist_birkhoffAverage_birkhoffAverage _ _ _ _ _ _).trans_le <| by
    gcongr; apply dist_birkhoffSum_birkhoffSum_le

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) / ↑n ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / ↑n

Tactic:
gcongr

Result:
case hab
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))

Proof state:
case hab
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))

Tactic:
apply dist_birkhoffSum_birkhoffSum_le

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
lemma thickening_biUnion {ι : Type*} (δ : ℝ) (f : ι → Set α) (I : Set ι) :
    thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, thickening δ (f i)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Type u_2
δ : ℝ
f : ι → Set α
I : Set ι
⊢ thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, thickening δ (f i)

Tactic:
simp only [thickening_iUnion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem tail_attach (xs : List α) :
    xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩)

Proof state:
α : Type u_1
xs : List α
⊢ xs.attach.tail =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.tail.attach

Tactic:
cases xs <;> simp

Result:
no goals