harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem BinaryCofan.isVanKampen_mk {X Y : C} (c : BinaryCofan X Y)
    (cofans : ∀ X Y : C, BinaryCofan X Y) (colimits : ∀ X Y, IsColimit (cofans X Y))
    (cones : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PullbackCone f g)
    (limits : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), IsLimit (cones f g))
    (h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt)
      (_ : αX ≫ c.inl = (cofans X' Y').inl ≫ f) (_ : αY ≫ c.inr = (cofans X' Y').inr ≫ f),
      IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr)
    (h₂ : ∀ {Z : C} (f : Z ⟶ c.pt),
      IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)) :
    IsVanKampenColimit c

Proof state:
case mp.intro.intro.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inl (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) c.inl

Tactic:
haveI : IsIso (𝟙 X') := inferInstance

Result:
case mp.intro.intro.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
this : IsIso (𝟙 X')
⊢ IsPullback c'.inl (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) c.inl
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_eval_two (n : ℤ) : (C R n).eval 2 = 2

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (↑n + 1)) = 2
ih2 : eval 2 (C R ↑n) = 2
⊢ eval 2 (C R (↑n + 2)) = 2

Tactic:
simp [C_add_two, ih1, ih2]

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (↑n + 1)) = 2
ih2 : eval 2 (C R ↑n) = 2
⊢ 2 * 2 - 2 = 2

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (↑n + 1)) = 2
ih2 : eval 2 (C R ↑n) = 2
⊢ 2 * 2 - 2 = 2

Tactic:
norm_num

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (-↑n)) = 2
ih2 : eval 2 (C R (-↑n + 1)) = 2
⊢ eval 2 (C R (-↑n - 1)) = 2

Tactic:
simp [C_sub_one, -C_neg, ih1, ih2]

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (-↑n)) = 2
ih2 : eval 2 (C R (-↑n + 1)) = 2
⊢ 2 * 2 - 2 = 2

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ eval 2 (C R 1) = 2

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 2 (C R 0) = 2

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 2 (C R n) = 2

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 => simp [C_add_two, ih1, ih2]; norm_num
| neg_add_one n ih1 ih2 => simp [C_sub_one, -C_neg, ih1, ih2]; norm_num

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (-↑n)) = 2
ih2 : eval 2 (C R (-↑n + 1)) = 2
⊢ 2 * 2 - 2 = 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithBot.lt_ofDual_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    x < WithBot.ofDual y ↔ y < x.toDual

Proof state:
α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < WithBot.ofDual y ↔ y < WithTop.toDual x

Tactic:
cases x <;> cases y <;> simp [lt_toDual]

Result:
no goals
-- Mathlib/FieldTheory/Differential/Basic.lean
lemma logDeriv_eq_zero : logDeriv a = 0 ↔ a′ = 0 :=
  ⟨fun h ↦ by simp only [logDeriv, _root_.div_eq_zero_iff] at h; rcases h with h|h <;> simp [h],
  fun h ↦ by unfold logDeriv at *; simp [h]⟩

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0 ∨ a = 0
⊢ a′ = 0

Tactic:
rcases h with h|h <;> simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0
⊢ logDeriv a = 0

Tactic:
unfold logDeriv at *

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0
⊢ a′ / a = 0

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0
⊢ a′ / a = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : logDeriv a = 0
⊢ a′ = 0

Tactic:
simp only [logDeriv, _root_.div_eq_zero_iff] at h

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0 ∨ a = 0
⊢ a′ = 0
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_pi_le_of_le {π : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (π b)]
    {s : ∀ b : β, Set (π b)} {c : ℝ≥0∞} (h : ∀ b, diam (s b) ≤ c) : diam (Set.pi univ s) ≤ c

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
x : (i : β) → π i
hx : x ∈ univ.pi s
y : (i : β) → π i
hy : y ∈ univ.pi s
⊢ ∀ (b : β), edist (x b) (y b) ≤ c

Tactic:
rw [mem_univ_pi] at hx hy

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
⊢ ∀ (b : β), edist (x b) (y b) ≤ c

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
⊢ ∀ (b : β), edist (x b) (y b) ≤ c

Tactic:
exact fun b => diam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)

Result:
no goals

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
⊢ diam (univ.pi s) ≤ c

Tactic:
refine diam_le fun x hx y hy => edist_pi_le_iff.mpr ?_

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
x : (i : β) → π i
hx : x ∈ univ.pi s
y : (i : β) → π i
hy : y ∈ univ.pi s
⊢ ∀ (b : β), edist (x b) (y b) ≤ c
-- Mathlib/Data/Set/Function.lean
/-- **Vertical line test** for functions.

Let `s : Set (β × γ)` be a set in a product. Assume that `s` maps bijectively to the first factor.
Then `s` is the graph of some function `f : β → γ`. -/
lemma exists_eq_mgraphOn_univ {s : Set (β × γ)}
    (hs₁ : Bijective (Prod.fst ∘ (Subtype.val : s → β × γ))) : ∃ f : β → γ, s = univ.graphOn f

Proof state:
β : Type u_2
γ : Type u_3
s : Set (β × γ)
hs₁ : Bijective (Prod.fst ∘ Subtype.val)
⊢ ∃ f, s = graphOn f univ

Tactic:
simpa using exists_range_eq_graphOn_univ hs₁.surjective
  fun a b h ↦ congr_arg (Prod.snd ∘ (Subtype.val : s → β × γ)) (hs₁.injective h)

Result:
no goals
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem Prime.sum_four_squares {p : ℕ} (hp : p.Prime) :
    ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.inr
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
⊢ False

Tactic:
by_cases hm : 2 ∣ m

Result:
case pos
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : 2 ∣ m
⊢ False

case neg
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
⊢ False
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_ΨSq (n : ℤ) : (W.baseChange B).ΨSq n = ((W.baseChange A).ΨSq n).map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W.baseChange B).ΨSq n = Polynomial.map (↑f) ((W.baseChange A).ΨSq n)

Tactic:
rw [← map_ΨSq, map_baseChange]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean
theorem universallyInjective_eq :
    @UniversallyInjective = universally (topologically (Injective ·))

Proof state:
⊢ @UniversallyInjective =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x).universally

Tactic:
ext X Y f

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x).universally f

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x).universally f

Tactic:
rw [universallyInjective_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem splitOnP_eq_splitOnPTR : @splitOnP = @splitOnPTR

Proof state:
case h.h.h.cons
α : Type u_1
P : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α) (r : Array (List α)), splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse
acc : Array α
r : Array (List α)
⊢ (bif P x then splitOnPTR.go P xs #[] (r.push acc.toList) else splitOnPTR.go P xs (acc.push x) r) =
    r.toList ++ if P x = true then acc.toList :: splitOnP.go P xs [] else splitOnP.go P xs (x :: acc.toList.reverse)

Tactic:
cases P x <;> simp [*]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α) (r : Array (List α)),
    splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse

Tactic:
intro xs acc r

Result:
case h.h.h
α : Type u_1
P : α → Bool
l xs : List α
acc : Array α
r : Array (List α)
⊢ splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse

Proof state:
⊢ @splitOnP = @splitOnPTR

Tactic:
funext α P l

Result:
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR P l

Proof state:
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR P l

Tactic:
simp [splitOnPTR]

Result:
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR.go P l #[] #[]

Proof state:
case h.h.h
α : Type u_1
P : α → Bool
l xs : List α
acc : Array α
r : Array (List α)
⊢ splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse

Tactic:
induction xs generalizing acc r with simp [splitOnP.go, splitOnPTR.go]
| cons x xs IH => cases P x <;> simp [*]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR.go P l #[] #[]

Tactic:
suffices ∀ xs acc r,
  splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse from
    (this l #[] #[]).symm

Result:
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α) (r : Array (List α)),
    splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse
-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem IsTranscendenceBasis.isAlgebraic [Nontrivial R] (hx : IsTranscendenceBasis R x) :
    Algebra.IsAlgebraic (adjoin R (range x)) A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
⊢ a ∈ range fun o => o.elim a x

Tactic:
exact ⟨none, rfl⟩

Result:
no goals

Proof state:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ _root_.IsAlgebraic (↥(adjoin R (range x))) a

Tactic:
rw [← not_iff_comm.1 (hx.1.option_iff _).symm]

Result:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o => o.elim a x

Proof state:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ ∀ (x_1 : A), _root_.IsAlgebraic (↥(adjoin R (range x))) x_1

Tactic:
intro a

Result:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ _root_.IsAlgebraic (↥(adjoin R (range x))) a

Proof state:
case intro
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
y : ι
⊢ x y ∈ range fun o => o.elim a x

Tactic:
exact ⟨some y, rfl⟩

Result:
no goals
-- Mathlib/Data/PNat/Defs.lean
theorem div_coe (m k : ℕ+) :
    (div m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) ((m : ℕ) / (k : ℕ)).pred ((m : ℕ) / (k : ℕ))

Proof state:
m k : ℕ+
⊢ m.div k = if ↑m % ↑k = 0 then (↑m / ↑k).pred else ↑m / ↑k

Tactic:
dsimp [div, modDiv]

Result:
m k : ℕ+
⊢ (k.modDivAux (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Proof state:
m k : ℕ+
⊢ (k.modDivAux (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl

Result:
no goals

Proof state:
case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = if n + 1 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
rw [if_neg n.succ_ne_zero]

Result:
case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = ↑m / ↑k

Proof state:
case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = ↑m / ↑k

Tactic:
rfl

Result:
no goals

Proof state:
case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = ↑m / ↑k - 1

Tactic:
rfl

Result:
no goals

Proof state:
case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = if 0 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
rw [if_pos rfl]

Result:
case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = ↑m / ↑k - 1
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
lemma mFourier_norm : ‖mFourier n‖ = 1

Proof state:
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ = 1

Tactic:
apply le_antisymm

Result:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ ≤ 1

case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ 1 ≤ ‖mFourier n‖

Proof state:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ 1 ≤ ‖mFourier n‖

Tactic:
refine (le_of_eq ?_).trans ((mFourier n).norm_coe_le_norm fun _ ↦ 0)

Result:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ 1 = ‖(mFourier n) fun x => 0‖

Proof state:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
i : UnitAddTorus d
⊢ ‖(mFourier n) i‖ ≤ 1

Tactic:
simp only [mFourier, fourier_apply, ContinuousMap.coe_mk, norm_prod, Circle.norm_coe,
  Finset.prod_const_one, le_rfl]

Result:
no goals

Proof state:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ ≤ 1

Tactic:
refine (ContinuousMap.norm_le _ zero_le_one).mpr fun i ↦ ?_

Result:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
i : UnitAddTorus d
⊢ ‖(mFourier n) i‖ ≤ 1

Proof state:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ 1 = ‖(mFourier n) fun x => 0‖

Tactic:
simp only [mFourier, ContinuousMap.coe_mk, fourier_eval_zero, Finset.prod_const_one,
  CStarRing.norm_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem eq_of_glueDist_eq_zero (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (ε0 : 0 < ε) :
    ∀ p q : X ⊕ Y, glueDist Φ Ψ ε p q = 0 → p = q
  | .inl x, .inl y, h => by rw [eq_of_dist_eq_zero h]
  | .inl x, .inr y, h => by exfalso; linarith [le_glueDist_inl_inr Φ Ψ ε x y]
  | .inr x, .inl y, h => by exfalso; linarith [le_glueDist_inr_inl Φ Ψ ε x y]
  | .inr x, .inr y, h => by rw [eq_of_dist_eq_zero h]

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ False

Tactic:
linarith [le_glueDist_inr_inl Φ Ψ ε x y]

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ Sum.inr x = Sum.inl y

Tactic:
exfalso

Result:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ False

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ Sum.inl x = Sum.inr y

Tactic:
exfalso

Result:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : Y
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) = 0
⊢ Sum.inr x = Sum.inr y

Tactic:
rw [eq_of_dist_eq_zero h]

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : X
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) = 0
⊢ Sum.inl x = Sum.inl y

Tactic:
rw [eq_of_dist_eq_zero h]

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False

Tactic:
linarith [le_glueDist_inl_inr Φ Ψ ε x y]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.mul (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) :
    HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x

Tactic:
have := (HasStrictFDerivAt.mul' hc hd).hasStrictDerivAt

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
this : HasStrictDerivAt (fun y => c y * d y) ((c x • smulRight 1 d' + (smulRight 1 c').smulRight (d x)) 1) x
⊢ HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
this : HasStrictDerivAt (fun y => c y * d y) ((c x • smulRight 1 d' + (smulRight 1 c').smulRight (d x)) 1) x
⊢ HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x

Tactic:
rwa [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, one_smul, one_smul,
  add_comm] at this

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
protected lemma IsNClique.insert_erase
    (hs : G.IsNClique n s) (ha : ∀ w ∈ s \ {b}, G.Adj a w) (hb : b ∈ s) :
    G.IsNClique n (insert a (erase s b))

Proof state:
case zero
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
hs : G.IsNClique 0 s
⊢ G.IsNClique 0 (insert a (s.erase b))

Tactic:
exact False.elim <| not_mem_empty _ (isNClique_zero.1 hs ▸ hb)

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a b : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
⊢ G.IsNClique n (insert a (s.erase b))

Tactic:
cases n with
| zero => exact False.elim <| not_mem_empty _ (isNClique_zero.1 hs ▸ hb)
| succ _ => exact (hs.erase_of_mem hb).insert fun w h ↦ by aesop

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
n✝ : ℕ
hs : G.IsNClique (n✝ + 1) s
w : α
h : w ∈ s.erase b
⊢ G.Adj a w

Tactic:
aesop

Result:
no goals

Proof state:
case succ
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
n✝ : ℕ
hs : G.IsNClique (n✝ + 1) s
⊢ G.IsNClique (n✝ + 1) (insert a (s.erase b))

Tactic:
exact (hs.erase_of_mem hb).insert fun w h ↦ by aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getElem_mul {x y : BitVec w} {i : Nat} (h : i < w) :
    (x * y)[i] = (mulRec x y w)[i]

Proof state:
w : Nat
x y : BitVec w
i : Nat
h : i < w
⊢ (x * y)[i] = (x.mulRec y w)[i]

Tactic:
simp [mulRec_eq_mul_signExtend_setWidth]

Result:
no goals