harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem head?_enumFrom (n : Nat) (l : List α) :
    (enumFrom n l).head? = l.head?.map fun a => (n, a)

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (enumFrom n l).head? = Option.map (fun a => (n, a)) l.head?

Tactic:
simp [head?_eq_getElem?]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_map_eq_C {f : K[X]} {a : L} (h : f.map i = C a) : Splits i f :=
  letI := Classical.decEq L
  if ha : a = 0 then Or.inl (h.trans (ha.symm ▸ C_0))
  else
    Or.inr fun hg ⟨p, hp⟩ =>
      absurd hg.1 <|
        Classical.not_not.2 <|
          isUnit_iff_degree_eq_zero.2 <| by
            have := congr_arg degree hp
            rw [h, degree_C ha, degree_mul, @eq_comm (WithBot ℕ) 0,
                Nat.WithBot.add_eq_zero_iff] at this
            exact this.1

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
a : L
h : map i f = C a
this✝ : DecidableEq L := Classical.decEq L
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : (map i f).degree = (g✝ * p).degree
⊢ g✝.degree = 0

Tactic:
rw [h, degree_C ha, degree_mul, @eq_comm (WithBot ℕ) 0,
    Nat.WithBot.add_eq_zero_iff] at this

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
a : L
h : map i f = C a
this✝ : DecidableEq L := Classical.decEq L
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : g✝.degree = 0 ∧ p.degree = 0
⊢ g✝.degree = 0

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
a : L
h : map i f = C a
this✝ : DecidableEq L := Classical.decEq L
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : g✝.degree = 0 ∧ p.degree = 0
⊢ g✝.degree = 0

Tactic:
exact this.1

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
a : L
h : map i f = C a
this : DecidableEq L := Classical.decEq L
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
⊢ g✝.degree = 0

Tactic:
have := congr_arg degree hp

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
a : L
h : map i f = C a
this✝ : DecidableEq L := Classical.decEq L
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : (map i f).degree = (g✝ * p).degree
⊢ g✝.degree = 0
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma nil_copy {x' y' : V} {p : G.Walk x y} (hx : x = x') (hy : y = y') :
    (p.copy hx hy).Nil = p.Nil

Proof state:
V : Type u
G : SimpleGraph V
x y x' y' : V
p : G.Walk x y
hx : x = x'
hy : y = y'
⊢ (p.copy hx hy).Nil = p.Nil

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
x' y' : V
p : G.Walk x' y'
⊢ (p.copy ⋯ ⋯).Nil = p.Nil

Proof state:
V : Type u
G : SimpleGraph V
x' y' : V
p : G.Walk x' y'
⊢ (p.copy ⋯ ⋯).Nil = p.Nil

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem MellinConvergent.cpow_smul {f : ℝ → E} {s a : ℂ} :
    MellinConvergent (fun t => (t : ℂ) ^ a • f t) s ↔ MellinConvergent f (s + a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • (fun t => ↑t ^ a • f t) t = ↑t ^ (s + a - 1) • f t

Tactic:
simp_rw [← sub_add_eq_add_sub, cpow_add _ _ (ofReal_ne_zero.2 <| ne_of_gt ht), mul_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
⊢ MellinConvergent (fun t => ↑t ^ a • f t) s ↔ MellinConvergent f (s + a)

Tactic:
refine integrableOn_congr_fun (fun t ht => ?_) measurableSet_Ioi

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • (fun t => ↑t ^ a • f t) t = ↑t ^ (s + a - 1) • f t
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma rev_sub (a b : Fin n) : rev (a - b) = rev a + b

Proof state:
n : ℕ
a b : Fin n
⊢ (a - b).rev = a.rev + b

Tactic:
rw [rev_eq_iff, rev_add, rev_rev]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem DiscreteUnif.cauchy_le_pure {X : Type*} {uX : UniformSpace X}
    (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : ∃ x : X, α = pure x

Proof state:
case intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
α_le : α ×ˢ α ≤ 𝓤 X
⊢ ∃ x, α = pure x

Tactic:
rw [hX, bot_uniformity, le_principal_iff, mem_prod_iff] at α_le

Result:
case intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
α_le : ∃ t₁ ∈ α, ∃ t₂ ∈ α, t₁ ×ˢ t₂ ⊆ idRel
⊢ ∃ x, α = pure x

Proof state:
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
hα : Cauchy α
⊢ ∃ x, α = pure x

Tactic:
rcases hα with ⟨α_ne_bot, α_le⟩

Result:
case intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
α_le : α ×ˢ α ≤ 𝓤 X
⊢ ∃ x, α = pure x

Proof state:
case intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
α_le : ∃ t₁ ∈ α, ∃ t₂ ∈ α, t₁ ×ˢ t₂ ⊆ idRel
⊢ ∃ x, α = pure x

Tactic:
obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := α_le

Result:
case intro.intro.intro.intro.intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
S : Set X
hS : S ∈ α
T : Set X
hT : T ∈ α
H : S ×ˢ T ⊆ idRel
⊢ ∃ x, α = pure x

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
T : Set X
hT : T ∈ α
x : X
hS : {x} ∈ α
H : {x} ×ˢ T ⊆ idRel
⊢ ∃ x, α = pure x

Tactic:
exact ⟨x, α_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
S : Set X
hS : S ∈ α
T : Set X
hT : T ∈ α
H : S ×ˢ T ⊆ idRel
⊢ ∃ x, α = pure x

Tactic:
obtain ⟨x, rfl⟩ := eq_singleton_left_of_prod_subset_idRel (α_ne_bot.nonempty_of_mem hS)
  (Filter.nonempty_of_mem hT) H

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
uX : UniformSpace X
hX : uX = ⊥
α : Filter X
α_ne_bot : α.NeBot
T : Set X
hT : T ∈ α
x : X
hS : {x} ∈ α
H : {x} ×ˢ T ⊆ idRel
⊢ ∃ x, α = pure x
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem unit_leftAdjointUniq_hom {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x

Tactic:
rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
    (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x)

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
    (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x)

Tactic:
simp [← G.map_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit

Tactic:
ext x

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem nonneg_of_le {a b : α} (h : a ≤ b) : 0 ≤ variationOnFromTo f s a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : a ≤ b
⊢ 0 ≤ variationOnFromTo f s a b

Tactic:
simp only [variationOnFromTo, if_pos h, ENNReal.toReal_nonneg]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem seq_pure (f : Filter (α → β)) (a : α) : seq f (pure a) = map (fun g : α → β => g a) f

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g => g a) f

Tactic:
refine sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_

Result:
case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ (fun g => g a) '' s ⊆ s.seq t

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
g : α → β
hg : g ∈ s
⊢ (fun g => g a) g ∈ s.seq t

Tactic:
exact ⟨g, hg, a, ht, rfl⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g => g a) '' s ∈ f.seq (pure a)

Tactic:
rw [← seq_singleton]

Result:
case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ s.seq {a} ∈ f.seq (pure a)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ (fun g => g a) '' s ⊆ s.seq t

Tactic:
rintro b ⟨g, hg, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
g : α → β
hg : g ∈ s
⊢ (fun g => g a) g ∈ s.seq t

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ s.seq {a} ∈ f.seq (pure a)

Tactic:
exact seq_mem_seq hs singleton_mem_pure

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
⊢ f.seq (pure a) = map (fun g => g a) f

Tactic:
refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g => g a) '' s ∈ f.seq (pure a)

case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g => g a) f
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_apply (hf : Integrable f μ) {s : Set α} (hs : MeasurableSet s) :
    μ.withDensityᵥ f s = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ ↑(μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [withDensityᵥ, dif_pos hf]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      s =
    ∫ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      s =
    ∫ (x : α) in s, f x ∂μ

Tactic:
exact dif_pos hs

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
/-- If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs of commuting elements. -/
lemma card_commute_odd (hn : Odd n) :
    Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } = n * (n + 3)

Proof state:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ n + (n + (n + n * n)) = n * (n + 3)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
simp_rw [Nat.card_congr (OddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]

Result:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ n + (n + (n + n * n)) = n * (n + 3)

Proof state:
n : ℕ
hn : Odd n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
have hn' : NeZero n := ⟨hn.pos.ne'⟩

Result:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma add_pow_expChar_pow_of_commute (h : Commute x y) :
    (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
obtain _ | hprime := hR

Result:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n

case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Proof state:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n

Tactic:
simp only [one_pow, pow_one]

Result:
no goals

Proof state:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
simp [hr]

Result:
no goals

Proof state:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n

Result:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem opRingEquiv_symm_single [AddCommMonoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    AddMonoidAlgebra.opRingEquiv.symm (single x r) = op (single x r.unop)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
r : kᵐᵒᵖ
x : Gᵐᵒᵖ
⊢ AddMonoidAlgebra.opRingEquiv.symm (single x r) = op (single x (unop r))

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@[simp]
lemma coe_toTwoSided (I : Ideal R) (h) : (I.toTwoSided h : Set R) = I

Proof state:
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ∀ {x y : R}, x ∈ I → x * y ∈ I
⊢ ↑(I.toTwoSided h) = ↑I

Tactic:
simp [toTwoSided]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem invFun_eq_of_injective_of_rightInverse {g : β → α} (hf : Injective f)
    (hg : RightInverse g f) : invFun f = g :=
  funext fun b ↦
    hf
      (by
        rw [hg b]
        exact invFun_eq ⟨g b, hg b⟩)

Proof state:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)

Tactic:
rw [hg b]

Result:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b

Proof state:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b

Tactic:
exact invFun_eq ⟨g b, hg b⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem dart_fst_fiber_card_eq_degree [DecidableEq V] (v : V) :
    #{d : G.Dart | d.fst = v} = G.degree v

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
⊢ #(filter (fun d => d.toProd.1 = v) univ) = G.degree v

Tactic:
simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
  card_image_of_injective univ (G.dartOfNeighborSet_injective v)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Classical.lean
theorem dite_not [hn : Decidable (¬p)] (x : ¬p → α) (y : ¬¬p → α) :
    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x

Proof state:
case isTrue
p : Prop
α : Sort u_1
x : ¬p → α
y : ¬¬p → α
g : ¬p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Tactic:
simp [g]

Result:
no goals

Proof state:
p : Prop
α : Sort u_1
hn : Decidable ¬p
x : ¬p → α
y : ¬¬p → α
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Tactic:
cases hn <;> rename_i g

Result:
case isFalse
p : Prop
α : Sort u_1
x : ¬p → α
y : ¬¬p → α
g : ¬¬p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

case isTrue
p : Prop
α : Sort u_1
x : ¬p → α
y : ¬¬p → α
g : ¬p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Proof state:
case isFalse
p : Prop
α : Sort u_1
x : ¬p → α
y : ¬¬p → α
g : ¬¬p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Tactic:
simp [not_not.mp g]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem of_d_ne {i j : α} (h : i + 1 ≠ j) : (of X d sq).d i j = 0

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (of X d sq).d i j = 0

Tactic:
dsimp [of]

Result:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0) = 0

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0) = 0

Tactic:
rw [dif_neg h]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivative_inv {R} [CommRing R] (f : R⟦X⟧ˣ) :
    d⁄dX R ↑f⁻¹ = -(↑f⁻¹ : R⟦X⟧) ^ 2 * d⁄dX R f

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R⟦X⟧ˣ
⊢ (d⁄dX R) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (d⁄dX R) ↑f

Tactic:
apply Derivation.leibniz_of_mul_eq_one

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R⟦X⟧ˣ
⊢ ↑f⁻¹ * ↑f = 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R⟦X⟧ˣ
⊢ ↑f⁻¹ * ↑f = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem join_pmap_eq_pmap_join {f : ∀ a, p a → β} {x : Option (Option α)} (H) :
    (pmap (pmap f) x H).join = pmap f x.join fun a h ↦ H (some a) (mem_of_mem_join h) _ rfl

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option (Option α)
H : ∀ (a : Option α), a ∈ x → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ (pmap (pmap f) x H).join = pmap f x.join ⋯

Tactic:
rcases x with (_ | _ | x) <;> simp

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma tendsto_toReal_atBot : Tendsto EReal.toReal (𝓝[≠] ⊥) atBot

Proof state:
⊢ Tendsto toReal (𝓝[≠] ⊥) atBot

Tactic:
rw [nhdsWithin_bot, tendsto_map'_iff]

Result:
⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot

Proof state:
⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot

Tactic:
exact tendsto_id

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@[reassoc]
lemma Γevaluation_naturality (x : X) :
    Y.Γevaluation (f.base x) ≫ residueFieldMap f x =
      f.c.app (op ⊤) ≫ X.Γevaluation x :=
  evaluation_naturality f ⟨x, by simp only [Opens.map_top]; trivial⟩

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ (Opens.map f.base).obj ⊤

Tactic:
simp only [Opens.map_top]

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ ⊤
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem Submonoid.adjoin_eq_span_of_eq_span [Semiring F] [Module F K] [IsScalarTower F E K]
    (L : Submonoid K) {S : Set K} (h : (L : Set K) = span F S) :
    toSubmodule (adjoin E (L : Set K)) = span E S

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ span E ↑(span F S) = span E S

Tactic:
exact (span_le.mpr <| span_subset_span _ _ _).antisymm (span_mono subset_span)

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ toSubmodule (adjoin E ↑L) = span E S

Tactic:
rw [adjoin_eq_span, L.closure_eq, h]

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ span E ↑(span F S) = span E S
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_natCast (n : ℕ) : (n : HomogeneousLocalization 𝒜 x).val = n :=
  show val (Nat.unaryCast n) = _ by induction n <;> simp [Nat.unaryCast, *]

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
n : ℕ
⊢ n.unaryCast.val = ↑n

Tactic:
induction n <;> simp [Nat.unaryCast, *]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharNeTwoNF : W.c₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.c₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
rw [c₆, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_sixteen : cos (π / 16) = √(2 + √(2 + √2)) / 2

Proof state:
case e_x.e_a

⊢ 16 = 2 ^ 4

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ cos (π / 16) = √(2 + √(2 + √2)) / 2

Tactic:
trans cos (π / 2 ^ 4)

Result:
⊢ cos (π / 16) = cos (π / 2 ^ 4)


⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2

Proof state:
⊢ cos (π / 16) = cos (π / 2 ^ 4)

Tactic:
congr

Result:
case e_x.e_a

⊢ 16 = 2 ^ 4

Proof state:
⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem rank_comap {L : Type v} [Field L] (f : L →+* E) :
    Module.rank (A.comap f) L = relrank A f.fieldRange

Proof state:
E : Type v
inst✝¹ : Field E
A : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange

Tactic:
simpa only [lift_id] using A.lift_rank_comap f

Result:
no goals