harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Fib/Basic.lean
@[simp] lemma fib_eq_zero : ∀ {n}, fib n = 0 ↔ n = 0
| 0 => Iff.rfl
| 1 => Iff.rfl
| n + 2 => by simp [fib_add_two, fib_eq_zero]

Proof state:
n : ℕ
⊢ fib (n + 2) = 0 ↔ n + 2 = 0

Tactic:
simp [fib_add_two, fib_eq_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_eq_single {f : α →₀ M} (a : α) {g : α → M → N}
    (h₀ : ∀ b, f b ≠ 0 → b ≠ a → g b (f b) = 1) (h₁ : f a = 0 → g a 0 = 1) :
    f.prod g = g a (f a)

Proof state:
case refine_1
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
b : α
hb₁ : b ∈ f.support
hb₂ : b ≠ a
⊢ g b (f b) = 1

Tactic:
exact h₀ b (mem_support_iff.mp hb₁) hb₂

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a (f a) = 1

Tactic:
rw [h]

Result:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a 0 = 1

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
⊢ f.prod g = g a (f a)

Tactic:
refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)

Result:
case refine_1
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
b : α
hb₁ : b ∈ f.support
hb₂ : b ≠ a
⊢ g b (f b) = 1

case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : a ∉ f.support
⊢ g a (f a) = 1

Proof state:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a 0 = 1

Tactic:
exact h₁ h

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : a ∉ f.support
⊢ g a (f a) = 1

Tactic:
simp only [not_mem_support_iff] at h

Result:
case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : f a = 0
⊢ g a (f a) = 1
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem t2Space_iff_disjoint_nhds : T2Space X ↔ Pairwise fun x y : X => Disjoint (𝓝 x) (𝓝 y)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
x✝ : x ≠ y
⊢ (fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔ (fun x y => Disjoint (𝓝 x) (𝓝 y)) x y

Tactic:
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), exists_prop, ← exists_and_left,
  and_assoc, and_comm, and_left_comm]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun x y => Disjoint (𝓝 x) (𝓝 y)

Tactic:
refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
x✝ : x ≠ y
⊢ (fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔ (fun x y => Disjoint (𝓝 x) (𝓝 y)) x y
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem map_withDensity_abs_det_fderiv_eq_addHaar (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (h'f : Measurable f) :
    Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) =
      μ.restrict (f '' s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : Measurable f
⊢ Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)

Tactic:
apply Measure.ext fun t ht => ?_

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : Measurable f
t : Set E
ht : MeasurableSet t
⊢ (Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|)) t = (μ.restrict (f '' s)) t

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : Measurable f
t : Set E
ht : MeasurableSet t
⊢ (Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|)) t = (μ.restrict (f '' s)) t

Tactic:
rw [map_apply h'f ht, withDensity_apply _ (h'f ht), Measure.restrict_apply ht,
  restrict_restrict (h'f ht),
  lintegral_abs_det_fderiv_eq_addHaar_image μ ((h'f ht).inter hs)
    (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
  image_preimage_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
    foldl n f x = foldlM (m:=Id) n f x

Proof state:
α : Type u_1
n : Nat
f : α → Fin n → α
x : α
⊢ foldl n f x = foldlM n f x

Tactic:
induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
lemma neg_one_pow_eq_pow_mod_two (n : ℕ) : (-1 : R) ^ n = (-1) ^ (n % 2)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)

Tactic:
simp [sq]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ n = (-1) ^ (n % 2)

Tactic:
rw [← Nat.mod_add_div n 2, pow_add, pow_mul]

Result:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem edist_toL1_zero (f : α → β) (hf : Integrable f μ) :
    edist (hf.toL1 f) 0 = ∫⁻ a, edist (f a) 0 ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [edist_zero_right, Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
apply eLpNorm_one_eq_lintegral_enorm

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
/-- The set of points `a : α` such that `κ a ≪ η a` is measurable. -/
@[measurability]
lemma measurableSet_absolutelyContinuous (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    MeasurableSet {a | κ a ≪ η a}

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | κ a ≪ η a}

Tactic:
simp_rw [← singularPart_eq_zero_iff_absolutelyContinuous,
  singularPart_eq_zero_iff_measure_eq_zero]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a) = 0}

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a) = 0}

Tactic:
exact measurable_kernel_prod_mk_left (measurableSet_mutuallySingularSet κ η)
  (measurableSet_singleton 0)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean
/-- If a `LocalizerMorphism` is a localized equivalence, then any compatible functor
between the localized categories is an equivalence. -/
lemma isEquivalence [h : Φ.IsLocalizedEquivalence] [CatCommSq Φ.functor L₁ L₂ G] :
    G.IsEquivalence := (by
  rw [Φ.isEquivalence_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]
  exact h.isEquivalence)

Proof state:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedEquivalence
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ G.IsEquivalence

Tactic:
rw [Φ.isEquivalence_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]

Result:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedEquivalence
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

Proof state:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedEquivalence
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

Tactic:
exact h.isEquivalence

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem inv_head {i j} (w : NeWord G i j) : w.inv.head = w.last⁻¹

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv.head = w.last⁻¹

Tactic:
induction w <;> simp [inv, *]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem IsClique.card_le_chromaticNumber {s : Finset V} (h : G.IsClique s) :
    s.card ≤ G.chromaticNumber

Proof state:
case inl
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber = ⊤
⊢ ↑s.card ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case inr.intro
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : ↑G.chromaticNumber.toNat = G.chromaticNumber
n : ℕ
c : G.Colorable n
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
rw [← hc, Nat.cast_le]

Result:
case inr.intro
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : ↑G.chromaticNumber.toNat = G.chromaticNumber
n : ℕ
c : G.Colorable n
⊢ s.card ≤ G.chromaticNumber.toNat

Proof state:
case inr
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber ≠ ⊤
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
have hc' := hc

Result:
case inr
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc hc' : G.chromaticNumber ≠ ⊤
⊢ ↑s.card ≤ G.chromaticNumber

Proof state:
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
obtain (hc | hc) := eq_or_ne G.chromaticNumber ⊤

Result:
case inl
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber = ⊤
⊢ ↑s.card ≤ G.chromaticNumber

case inr
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber ≠ ⊤
⊢ ↑s.card ≤ G.chromaticNumber

Proof state:
case inl
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber = ⊤
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
rw [hc]

Result:
case inl
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber = ⊤
⊢ ↑s.card ≤ ⊤

Proof state:
case inr.intro
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber ≠ ⊤
n : ℕ
c : G.Colorable n
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
rw [← ENat.coe_toNat_eq_self] at hc

Result:
case inr.intro
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : ↑G.chromaticNumber.toNat = G.chromaticNumber
n : ℕ
c : G.Colorable n
⊢ ↑s.card ≤ G.chromaticNumber

Proof state:
case inr
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc hc' : G.chromaticNumber ≠ ⊤
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at hc'

Result:
case inr
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber ≠ ⊤
hc' : ∃ n, G.Colorable n
⊢ ↑s.card ≤ G.chromaticNumber

Proof state:
case inr.intro
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : ↑G.chromaticNumber.toNat = G.chromaticNumber
n : ℕ
c : G.Colorable n
⊢ s.card ≤ G.chromaticNumber.toNat

Tactic:
exact h.card_le_of_colorable (colorable_chromaticNumber c)

Result:
no goals

Proof state:
case inr
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber ≠ ⊤
hc' : ∃ n, G.Colorable n
⊢ ↑s.card ≤ G.chromaticNumber

Tactic:
obtain ⟨n, c⟩ := hc'

Result:
case inr.intro
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
hc : G.chromaticNumber ≠ ⊤
n : ℕ
c : G.Colorable n
⊢ ↑s.card ≤ G.chromaticNumber
-- Mathlib/RingTheory/Localization/NumDen.lean
lemma associated_num_den_inv (x : K) (hx : x ≠ 0) : Associated (num A x : A) (den A x⁻¹)

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
this : Associated (num A x⁻¹⁻¹) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)

Tactic:
rw [inv_inv] at this

Result:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
this : Associated (num A x) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
this : Associated (num A x) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)

Tactic:
exact this

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ Associated (num A x) ↑(den A x⁻¹)

Tactic:
have : Associated (num A x⁻¹⁻¹ : A) (den A x⁻¹) :=
  (associated_den_num_inv x⁻¹ (inv_ne_zero hx)).symm

Result:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
this : Associated (num A x⁻¹⁻¹) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma iterateFrobenius_one_apply : iterateFrobenius R p 1 x = x ^ p

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 1) x = x ^ p

Tactic:
rw [iterateFrobenius_def, pow_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
@[simp] lemma girth_bot : girth (⊥ : SimpleGraph α) = 0

Proof state:
α : Type u_1
⊢ ⊥.girth = 0

Tactic:
simp [girth]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_sub_lt (hd : degree p = degree q) (hp0 : p ≠ 0)
    (hlc : leadingCoeff p = leadingCoeff q) : degree (p - q) < degree p :=
  have hp : monomial (natDegree p) (leadingCoeff p) + p.erase (natDegree p) = p :=
    monomial_add_erase _ _
  have hq : monomial (natDegree q) (leadingCoeff q) + q.erase (natDegree q) = q :=
    monomial_add_erase _ _
  have hd' : natDegree p = natDegree q

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
⊢ (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
conv =>
  lhs
  rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
⊢ p.natDegree = q.natDegree

Tactic:
unfold natDegree

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Tactic:
rw [hd]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem sum_apply {α} (t : Finset α) (B : α → BilinForm R M) (v w : M) :
    (∑ i ∈ t, B i) v w = ∑ i ∈ t, B i v w

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_7
t : Finset α
B : α → BilinForm R M
v w : M
⊢ ((∑ i ∈ t, B i) v) w = ∑ i ∈ t, ((B i) v) w

Tactic:
simp only [coeFn_sum, Finset.sum_apply]

Result:
no goals
-- Mathlib/Topology/Order/T5.lean
theorem ordT5Nhd_mem_nhdsSet (hd : Disjoint s (closure t)) : ordT5Nhd s t ∈ 𝓝ˢ s :=
  bUnion_mem_nhdsSet fun x hx => ordConnectedComponent_mem_nhds.2 <| inter_mem
    (by
      rw [← mem_interior_iff_mem_nhds, interior_compl]
      exact disjoint_left.1 hd hx)
    (compl_ordConnectedSection_ordSeparatingSet_mem_nhds hd hx)

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s t : Set X
hd : Disjoint s (closure t)
x : X
hx : x ∈ s
⊢ tᶜ ∈ 𝓝 x

Tactic:
rw [← mem_interior_iff_mem_nhds, interior_compl]

Result:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s t : Set X
hd : Disjoint s (closure t)
x : X
hx : x ∈ s
⊢ x ∈ (closure t)ᶜ

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s t : Set X
hd : Disjoint s (closure t)
x : X
hx : x ∈ s
⊢ x ∈ (closure t)ᶜ

Tactic:
exact disjoint_left.1 hd hx

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Count.lean
theorem count_singleton' (a b : α) : count a [b] = if b = a then 1 else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ count a [b] = if b = a then 1 else 0

Tactic:
simp [count_cons]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem Preorder.ext {A B : Preorder α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) : A = B

Proof state:
case a.le.h.h.a
α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
exact H x y

Result:
no goals

Proof state:
α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y

Result:
case a.le.h.h.a
α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem not_mem_range_self {n : Nat} : n ∉ range n

Proof state:
n : Nat
⊢ ¬n ∈ range n

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none
    (hx : AlgebraicIndependent R x) :
    hx.mvPolynomialOptionEquivPolynomialAdjoin (X none) = Polynomial.X

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
hx : AlgebraicIndependent R x
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (X none) = Polynomial.X

Tactic:
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
  Polynomial.map_X]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem kerLift_injective : Injective (kerLift φ) := fun a b =>
  Quotient.inductionOn₂' a b fun a b (h : φ a = φ b) =>
    Quotient.sound' <| by rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]

Proof state:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ (leftRel φ.ker) a b

Tactic:
rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem list_prod_apply {I} (C : Set (I → Bool)) (x : C) (l : List (LocallyConstant C ℤ)) :
    l.prod x = (l.map (LocallyConstant.evalMonoidHom x)).prod

Proof state:
I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod

Tactic:
rw [← map_list_prod (LocallyConstant.evalMonoidHom x) l]

Result:
I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = (LocallyConstant.evalMonoidHom x) l.prod

Proof state:
I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = (LocallyConstant.evalMonoidHom x) l.prod

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_pow (n : Nat) : 1 ^ n = 1

Proof state:
n : Nat
⊢ 1 ^ n = 1

Tactic:
induction n with
| zero => rfl
| succ _ ih => rw [Nat.pow_succ, Nat.mul_one, ih]

Result:
no goals

Proof state:
case succ
n✝ : Nat
ih : 1 ^ n✝ = 1
⊢ 1 ^ (n✝ + 1) = 1

Tactic:
rw [Nat.pow_succ, Nat.mul_one, ih]

Result:
no goals

Proof state:
case zero

⊢ 1 ^ 0 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).hom =
    (Iso.refl (e.functor.obj ((𝟭 C).obj X))).hom

Tactic:
exact e.functor_unit_comp X

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X)

Tactic:
erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
    (Iso.refl _)]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).hom =
    (Iso.refl (e.functor.obj ((𝟭 C).obj X))).hom