harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Valuation/Integers.lean
lemma bijective_algebraMap_of_subsingleton_units_mrange (hv : Integers v O)
    [Subsingleton (MonoidHom.mrange v)ˣ] :
    Function.Bijective (algebraMap O F)

Proof state:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
x : F
⊢ v x ≤ 1

Tactic:
rcases eq_or_ne x 0 with rfl|hx

Result:
case inl
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
⊢ v 0 ≤ 1

case inr
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
x : F
hx : x ≠ 0
⊢ v x ≤ 1

Proof state:
case inr
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
x : F
hx : x ≠ 0
⊢ v x ≤ 1

Tactic:
exact (congr_arg Units.val (Subsingleton.elim (α := (MonoidHom.mrange v)ˣ)
  ((isUnit_iff_ne_zero.mpr hx).unit.map v.toMonoidHom.mrangeRestrict) 1)).le

Result:
no goals

Proof state:
case inl
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
⊢ v 0 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
⊢ Function.Bijective ⇑(algebraMap O F)

Tactic:
refine ⟨hv.hom_inj, fun x ↦ hv.exists_of_le_one ?_⟩

Result:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
x : F
⊢ v x ≤ 1
-- Mathlib/Data/List/Basic.lean
theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a

Proof state:
α : Type u
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a ++ replicate n a

Tactic:
rw [replicate_append_replicate]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma map_zero : (0 : Cochain K L n).map Φ = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ map 0 Φ = 0

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
    zipWith f (replicate n a) (replicate n b) = replicate n (f a b)

Proof state:
case zero
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
⊢ zipWith f (replicate 0 a) (replicate 0 b) = replicate 0 (f a b)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
n : Nat
ih : zipWith f (replicate n a) (replicate n b) = replicate n (f a b)
⊢ zipWith f (replicate (n + 1) a) (replicate (n + 1) b) = replicate (n + 1) (f a b)

Tactic:
simp [replicate_succ, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
n : Nat
⊢ zipWith f (replicate n a) (replicate n b) = replicate n (f a b)

Tactic:
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Lemmas.lean
@[simp, norm_cast]
lemma cast_pow (p : ℚ) (n : ℕ) : ↑(p ^ n) = (p ^ n : α)

Proof state:
α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p ^ n) = ↑p ^ n

Tactic:
rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
  ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_zsmul (m : ℤ) (x : 𝕎 R) : truncateFun n (m • x) = m • truncateFun n x

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
⊢ truncateFun n (m • x) = m • truncateFun n x

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma functorPushforward_equivalence_eq_pullback {U : C} (S : Sieve U) :
    Sieve.functorPushforward e.inverse (Sieve.functorPushforward e.functor S) =
      Sieve.pullback (e.unitInv.app U) S

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
U : C
S : Sieve U
⊢ functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
U : C
S : Sieve U
Y✝ : C
f✝ : Y✝ ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f✝ ↔ (pullback (e.unitInv.app U) S).arrows f✝

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
U : C
S : Sieve U
Y✝ : C
f✝ : Y✝ ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f✝ ↔ (pullback (e.unitInv.app U) S).arrows f✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Part.lean
theorem mod_get_eq [Mod α] (a b : Part α) (hab : Dom (a % b)) :
    (a % b).get hab = a.get (left_dom_of_mod_dom hab) % b.get (right_dom_of_mod_dom hab)

Proof state:
α : Type u_1
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a % b).get hab = a.get ⋯ % b.get ⋯

Tactic:
simp [mod_def]

Result:
α : Type u_1
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a.bind fun y => map (fun x => y % x) b).get ⋯ = a.get ⋯ % b.get ⋯

Proof state:
α : Type u_1
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a.bind fun y => map (fun x => y % x) b).get ⋯ = a.get ⋯ % b.get ⋯

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_const [CompleteSpace E] (c : E) : ∫ _ in s, c ∂μ = (μ s).toReal • c

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s : Set X
μ : Measure X
inst✝ : CompleteSpace E
c : E
⊢ ∫ (x : X) in s, c ∂μ = (μ s).toReal • c

Tactic:
rw [integral_const, Measure.restrict_apply_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_directed {f : End R M} {μ : R} {k : ℕ∞} :
    Directed (· ≤ ·) (fun l : {l : ℕ // l ≤ k} ↦ f.genEigenspace μ l)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
aux : Monotone fun x => ↑↑x
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun l => (f.genEigenspace μ) ↑↑l

Tactic:
exact ((genEigenspace f μ).monotone.comp aux).directed_le

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun l => (f.genEigenspace μ) ↑↑l

Tactic:
have aux : Monotone ((↑) : {l : ℕ // l ≤ k} → ℕ∞) := fun x y h ↦ by simpa using h

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
aux : Monotone fun x => ↑↑x
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun l => (f.genEigenspace μ) ↑↑l

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x y : { l // ↑l ≤ k }
h : x ≤ y
⊢ (fun x => ↑↑x) x ≤ (fun x => ↑↑x) y

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem comp_liftAddHom {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ]
    (g : γ →+ δ) (f : ∀ i, β i →+ γ) :
    g.comp (liftAddHom (β := β) f) = liftAddHom (β := β) fun a => g.comp (f a) :=
  (liftAddHom (β := β)).symm_apply_eq.1 <|
    funext fun a => by
      rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
δ : Type u_1
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : AddCommMonoid γ
inst✝ : AddCommMonoid δ
g : γ →+ δ
f : (i : ι) → β i →+ γ
a : ι
⊢ liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)

Tactic:
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem ssubset_iff_exists_subset_erase {s t : Finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊂ t
⊢ ∃ a ∈ t, s ⊆ t.erase a

Tactic:
obtain ⟨a, ht, hs⟩ := not_subset.1 h.2

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊂ t
a : α
ht : a ∈ t
hs : a ∉ s
⊢ ∃ a ∈ t, s ⊆ t.erase a

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊂ t
a : α
ht : a ∈ t
hs : a ∉ s
⊢ ∃ a ∈ t, s ⊆ t.erase a

Tactic:
exact ⟨a, ht, subset_erase.2 ⟨h.1, hs⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

Tactic:
refine ⟨fun h => ?_, fun ⟨a, ha, h⟩ => ssubset_of_subset_of_ssubset h <| erase_ssubset ha⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊂ t
⊢ ∃ a ∈ t, s ⊆ t.erase a
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
lemma norm_innerSL_le : ‖innerSL 𝕜 (E := E)‖ ≤ 1 :=
  ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)

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

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f ≠ [] ↔ l ≠ []

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f ≠ [] ↔ l ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_zero_eq_constantCoeff : ⇑(coeff R 0) = constantCoeff R

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(coeff R 0) = ⇑(constantCoeff R)

Tactic:
rw [coeff, Finsupp.single_zero]

Result:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.coeff R 0) = ⇑(constantCoeff R)

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.coeff R 0) = ⇑(constantCoeff R)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
/-- A global integer is in the local integers. -/
lemma coe_mem_adicCompletionIntegers (r : R) :
    (r : adicCompletion K v) ∈ adicCompletionIntegers K v

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ ↑r ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, valuedAdicCompletion_eq_valuation, valuation_eq_intValuationDef]

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ v.intValuationDef r ≤ 1

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ v.intValuationDef r ≤ 1

Tactic:
exact intValuation_le_one v r

Result:
no goals
-- Mathlib/Data/Complex/Determinant.lean
theorem linearEquiv_det_conjAe : LinearEquiv.det conjAe.toLinearEquiv = -1

Proof state:
⊢ LinearEquiv.det conjAe.toLinearEquiv = -1

Tactic:
rw [← Units.eq_iff, LinearEquiv.coe_det, AlgEquiv.toLinearEquiv_toLinearMap, det_conjAe,
  Units.coe_neg_one]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem is_rat (q : ℚ_[p]) : ∃ q' : ℚ, ‖q‖ = q'

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ∃ q', ‖q‖ = ↑q'

Tactic:
exact if h : q = 0 then ⟨0, by simp [h]⟩
else
  let ⟨n, hn⟩ := padicNormE.image h
  ⟨_, hn⟩

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
h : q = 0
⊢ ‖q‖ = ↑0

Tactic:
simp [h]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ∃ q', ‖q‖ = ↑q'

Tactic:
classical
exact if h : q = 0 then ⟨0, by simp [h]⟩
else
  let ⟨n, hn⟩ := padicNormE.image h
  ⟨_, hn⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k}
    (not_mem : (toInsert.map Sigma.fst).contains k = false) :
    getValueCastD k (insertList l toInsert) fallback = getValueCastD k l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
fallback : β k
not_mem : (List.map Sigma.fst toInsert).contains k = false
⊢ getValueCastD k (insertList l toInsert) fallback = getValueCastD k l fallback

Tactic:
rw [getValueCastD_eq_getValueCast?, getValueCastD_eq_getValueCast?,
  getValueCast?_insertList_of_contains_eq_false not_mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_append (f : α → β) : ∀ l₁ l₂, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (l₁ l₂ : List α), map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Tactic:
intro l₁

Result:
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
⊢ ∀ (l₂ : List α), map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
⊢ ∀ (l₂ : List α), map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Tactic:
induction l₁ <;> intros <;> simp_all

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem two_zsmul_oangle_eq {s : Sphere P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
    (hp₃ : p₃ ∈ s) (hp₄ : p₄ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₄ : p₂ ≠ p₄) (hp₃p₁ : p₃ ≠ p₁)
    (hp₃p₄ : p₃ ≠ p₄) : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ 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)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
rw [oangle, oangle, ← vsub_sub_vsub_cancel_right p₁ p₂ s.center, ←
    vsub_sub_vsub_cancel_right p₄ p₂ s.center,
    o.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq _ _ _ _ hp₂ hp₃ hp₁ hp₄] <;>
  simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]

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)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₄ : p₄ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄

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)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
protected lemma le_total : a ≤ b ∨ b ≤ a

Proof state:
a b : ℚ
⊢ a ≤ b ∨ b ≤ a

Tactic:
simpa only [← Rat.le_iff_sub_nonneg, neg_sub] using Rat.nonneg_total (b - a)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIdIso_inv_fst :
    (pullbackDiagonalMapIdIso f g i).inv ≫ pullback.fst _ _ = pullback.fst _ _ ≫ f

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) = fst f g ≫ f

Tactic:
rw [Iso.inv_comp_eq, ← Category.comp_id (pullback.fst _ _), ← diagonal_fst i,
  pullback.condition_assoc]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ fst i i =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g ≫ f

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ fst i i =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma scott_eq_upper_of_completeLinearOrder : scott α univ = upper α

Proof state:
case a.h.a
α : Type u_1
inst✝ : CompleteLinearOrder α
this✝ : TopologicalSpace α := upper α
U : Set α
this : TopologicalSpace α := scott α univ
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
rw [@isOpen_iff_Iic_compl_or_univ _ _ (scott α univ) ({ topology_eq_scott := rfl }) U]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLinearOrder α
⊢ scott α univ = upper α

Tactic:
letI := upper α

Result:
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
⊢ scott α univ = upper α

Proof state:
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
⊢ scott α univ = upper α

Tactic:
ext U

Result:
case a.h.a
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen U ↔ IsOpen U

Proof state:
case a.h.a
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen U ↔ IsOpen U

Tactic:
rw [@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α)
  ({ topology_eq_upperTopology := rfl }) U]

Result:
case a.h.a
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Proof state:
case a.h.a
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
letI := scott α univ

Result:
case a.h.a
α : Type u_1
inst✝ : CompleteLinearOrder α
this✝ : TopologicalSpace α := upper α
U : Set α
this : TopologicalSpace α := scott α univ
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U
-- Mathlib/Data/Option/NAry.lean
theorem map₂_left_comm {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
    (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) :
    map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)

Tactic:
cases a <;> cases b <;> cases c <;> simp [h_left_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem pow_rpow_inv_natCast (hx : 0 ≤ x) (hn : n ≠ 0) : (x ^ n) ^ (n⁻¹ : ℝ) = x

Proof state:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]

Result:
no goals

Proof state:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn

Result:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x
-- Mathlib/Order/Lattice.lean
theorem inf_sup_right (a b c : α) : (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

Tactic:
simp only [inf_sup_left, inf_comm _ c, eq_self_iff_true]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) :
    X.δ (Fin.castSucc i) ≫ X.σ j.succ = X.σ j ≫ X.δ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ j.succ) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_le H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.δ i.castSucc ≫ X.σ j.succ = X.σ j ≫ X.δ i

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ j.succ) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_flatten (f : α → β → β) (b : β) (L : Array (Array α)) :
    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b

Proof state:
case of
α : Type u_1
β : Type u_2
f : α → β → β
b : β
xss✝ : List (List α)
⊢ foldr f b (List.map List.toArray xss✝).toArray.flatten =
    foldr (fun l b => foldr f b l) b (List.map List.toArray xss✝).toArray

Tactic:
simp [List.foldr_flatten, List.foldr_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
L : Array (Array α)
⊢ foldr f b L.flatten = foldr (fun l b => foldr f b l) b L

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
β : Type u_2
f : α → β → β
b : β
xss✝ : List (List α)
⊢ foldr f b (List.map List.toArray xss✝).toArray.flatten =
    foldr (fun l b => foldr f b l) b (List.map List.toArray xss✝).toArray
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Iic : x ∈ Iic b ↔ x ≤ b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
rw [Iic, ← Finset.mem_def, Finset.mem_Iic]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.int_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℤ) :
    f (n * c - x) = (n.negOnePow : ℤ) * f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : Ring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℤ
⊢ f (↑n * c - x) = ↑↑n.negOnePow * f (-x)

Tactic:
simpa only [zsmul_eq_mul] using h.zsmul_sub_eq n

Result:
no goals