harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iExsUnique [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M} :
    BoundedFormula.Realize (φ.iExsUnique γ) v v' ↔
      ∃! (i : γ → M), φ.Realize (Sum.elim v i)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v

Tactic:
congr

Result:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Proof state:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExsUnique γ φ) v v' ↔ ∃! i, φ.Realize (Sum.elim v i)

Tactic:
rw [← Formula.realize_iExsUnique, iff_iff_eq]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem isUnit_iff_constantCoeff {φ : MvPowerSeries σ R} :
    IsUnit φ ↔ IsUnit (constantCoeff σ R φ)

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
hu : ↑u = (constantCoeff σ R) φ
⊢ IsUnit φ

Tactic:
exact ⟨⟨_, φ.invOfUnit u, mul_invOfUnit φ u hu.symm, invOfUnit_mul φ u hu.symm⟩, rfl⟩

Result:
no goals

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit ((constantCoeff σ R) φ) → IsUnit φ

Tactic:
intro ⟨u, hu⟩

Result:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
hu : ↑u = (constantCoeff σ R) φ
⊢ IsUnit φ

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ → IsUnit ((constantCoeff σ R) φ)

Tactic:
exact IsUnit.map _

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ ↔ IsUnit ((constantCoeff σ R) φ)

Tactic:
constructor

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ → IsUnit ((constantCoeff σ R) φ)

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit ((constantCoeff σ R) φ) → IsUnit φ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
    Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
      ⟨i, h⟩

Proof state:
n i : Nat
h : i < n + 1
⊢ ⟨i + 1, ⋯⟩.pred ⋯ = ⟨i, h⟩

Tactic:
simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Comon_.lean
theorem comul_counit_hom {Z : C} (f : M.X ⟶ Z) : M.comul ≫ (f ⊗ M.counit) = f ≫ (ρ_ Z).inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Comon_ C
Z : C
f : M.X ⟶ Z
⊢ M.comul ≫ (f ⊗ M.counit) = f ≫ (ρ_ Z).inv

Tactic:
rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
    getKey? a l = (getEntry? a l).map (·.1)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
⊢ getKey? a l = Option.map (fun x => x.fst) (getEntry? a l)

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
⊢ getKey? a [] = Option.map (fun x => x.fst) (getEntry? a [])

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : getKey? a tail✝ = Option.map (fun x => x.fst) (getEntry? a tail✝)
⊢ getKey? a (⟨k✝, v✝⟩ :: tail✝) = Option.map (fun x => x.fst) (getEntry? a (⟨k✝, v✝⟩ :: tail✝))

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : getKey? a l = Option.map (fun x => x.fst) (getEntry? a l)
⊢ getKey? a (⟨k, v⟩ :: l) = Option.map (fun x => x.fst) (getEntry? a (⟨k, v⟩ :: l))

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : getKey? a l = Option.map (fun x => x.fst) (getEntry? a l)
h : (k == a) = false
⊢ getKey? a (⟨k, v⟩ :: l) = Option.map (fun x => x.fst) (getEntry? a (⟨k, v⟩ :: l))

case true
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : getKey? a l = Option.map (fun x => x.fst) (getEntry? a l)
h : (k == a) = true
⊢ getKey? a (⟨k, v⟩ :: l) = Option.map (fun x => x.fst) (getEntry? a (⟨k, v⟩ :: l))

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : getKey? a l = Option.map (fun x => x.fst) (getEntry? a l)
h : (k == a) = false
⊢ getKey? a (⟨k, v⟩ :: l) = Option.map (fun x => x.fst) (getEntry? a (⟨k, v⟩ :: l))

Tactic:
rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih]

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : getKey? a l = Option.map (fun x => x.fst) (getEntry? a l)
h : (k == a) = true
⊢ getKey? a (⟨k, v⟩ :: l) = Option.map (fun x => x.fst) (getEntry? a (⟨k, v⟩ :: l))

Tactic:
rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some']

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
⊢ getKey? a [] = Option.map (fun x => x.fst) (getEntry? a [])

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.eventually_forall_of_forall_eventually {x₀ : X} {K : Set Y} (hK : IsCompact K)
    {P : X → Y → Prop} (hP : ∀ y ∈ K, ∀ᶠ z : X × Y in 𝓝 (x₀, y), P z.1 z.2) :
    ∀ᶠ x in 𝓝 x₀, ∀ y ∈ K, P x y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Tactic:
simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Tactic:
exact hP.curry.mono fun _ h ↦ h.self_of_nhdsSet

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem deterministic_congr {f g : α → β} {hf : Measurable f} (h : f = g) :
    deterministic f hf = deterministic g (h ▸ hf)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → β
hf : Measurable f
h : f = g
⊢ deterministic f hf = deterministic g ⋯

Tactic:
conv_lhs => enter [1]; rw [h]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLEMk_comp_ofMkLE {B A₁ A₂ : C} (f : A₁ ⟶ B) [Mono f] (g : A₂ ⟶ B) [Mono g]
    (X : Subobject B) (h₁ : mk f ≤ mk g) (h₂ : mk g ≤ X) :
    ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp underlying,
  assoc, Iso.hom_inv_id_assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_setIfInBounds (as : Array α) (i : Nat) (v : α) (j : Nat)
    (hj : j < (as.setIfInBounds i v).size) :
    (as.setIfInBounds i v)[j]'hj = if i = j then v else as[j]'(by simpa using hj)

Proof state:
case isFalse
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
h✝ : ¬i < as.size
⊢ as[j] = if i = j then v else as[j]

Tactic:
simp only [size_setIfInBounds] at hj

Result:
case isFalse
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj✝ : j < (as.setIfInBounds i v).size
h✝ : ¬i < as.size
hj : j < as.size
⊢ as[j] = if i = j then v else as[j]

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
⊢ (if h : i < as.size then as.set i v h else as)[j] = if i = j then v else as[j]

Tactic:
split

Result:
case isTrue
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
h✝ : i < as.size
⊢ (as.set i v h✝)[j] = if i = j then v else as[j]

case isFalse
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
h✝ : ¬i < as.size
⊢ as[j] = if i = j then v else as[j]

Proof state:
α : Type ?u.129880
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
⊢ j < as.size

Tactic:
simpa using hj

Result:
no goals

Proof state:
case isTrue
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
h✝ : i < as.size
⊢ (as.set i v h✝)[j] = if i = j then v else as[j]

Tactic:
simp [getElem_set]

Result:
no goals

Proof state:
case isFalse.hnc
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj✝ : j < (as.setIfInBounds i v).size
h✝ : ¬i < as.size
hj : j < as.size
⊢ ¬i = j

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
⊢ (as.setIfInBounds i v)[j] = if i = j then v else as[j]

Tactic:
simp only [setIfInBounds]

Result:
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
⊢ (if h : i < as.size then as.set i v h else as)[j] = if i = j then v else as[j]

Proof state:
case isFalse
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj✝ : j < (as.setIfInBounds i v).size
h✝ : ¬i < as.size
hj : j < as.size
⊢ as[j] = if i = j then v else as[j]

Tactic:
rw [if_neg]

Result:
case isFalse.hnc
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj✝ : j < (as.setIfInBounds i v).size
h✝ : ¬i < as.size
hj : j < as.size
⊢ ¬i = j
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem neg_smul : -g • z = g • z

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ -g • z = g • z

Tactic:
ext1

Result:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ ↑(-g • z) = ↑(g • z)

Proof state:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ ↑(-g • z) = ↑(g • z)

Tactic:
change _ / _ = _ / _

Result:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (-g) z / denom (-g) z = num g z / denom g z

Proof state:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (-(↑(↑↑g 0 0) * ↑z) + -↑(↑↑g 0 1)) * (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑(↑↑g 0 0) * ↑z + ↑(↑↑g 0 1)) * (-(↑(↑↑g 1 0) * ↑z) + -↑(↑↑g 1 1))

Tactic:
ring_nf

Result:
no goals

Proof state:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (-g) z / denom (-g) z = num g z / denom g z

Tactic:
field_simp [denom_ne_zero]

Result:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (-g) z * denom g z = num g z * denom (-g) z

Proof state:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (-g) z * denom g z = num g z * denom (-g) z

Tactic:
simp only [num, denom, Complex.ofReal_neg, neg_mul, GLPos.coe_neg_GL, Units.val_neg, neg_apply]

Result:
case h
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (-(↑(↑↑g 0 0) * ↑z) + -↑(↑↑g 0 1)) * (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑(↑↑g 0 0) * ↑z + ↑(↑↑g 0 1)) * (-(↑(↑↑g 1 0) * ↑z) + -↑(↑↑g 1 1))
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem norm_iteratedFDeriv_le (n : ℕ) (x : (i : ι) → E i) :
    ‖iteratedFDeriv 𝕜 n f x‖
      ≤ Nat.descFactorial (Fintype.card ι) n * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
⊢ ‖f.iteratedFDeriv n x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

Tactic:
exact f.norm_iteratedFDeriv_le' n x

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
⊢ ‖iteratedFDeriv 𝕜 n (⇑f) x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

Tactic:
rw [f.iteratedFDeriv_eq]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
⊢ ‖f.iteratedFDeriv n x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleType_finRotate {n : ℕ} : cycleType (finRotate (n + 2)) = {n + 2}

Proof state:
n : ℕ
⊢ ↑[n + 2] = {n + 2}

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ (finRotate (n + 2)).cycleType = {n + 2}

Tactic:
rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]

Result:
n : ℕ
⊢ ↑[n + 2] = {n + 2}
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem HasStrictDerivAt.div (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x)
    (hx : d x ≠ 0) : HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') * (d x * d x ^ 2) = (c' * d x ^ 2 + -(c x * d' * d x)) * d x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / d x ^ 2 = c' * (Inv.inv ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')

Tactic:
field_simp

Result:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') * (d x * d x ^ 2) = (c' * d x ^ 2 + -(c x * d' * d x)) * d x ^ 2

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x

Tactic:
convert hc.mul ((hasStrictDerivAt_inv hx).comp x hd) using 1

Result:
case h.e'_8
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (fun y => c y / d y) = fun y => c y * (Inv.inv ∘ d) y

case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / d x ^ 2 = c' * (Inv.inv ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem ContMDiff.extend_one [T2Space M] [One M'] {n : WithTop ℕ∞} {U : Opens M} {f : U → M'}
    (supp : HasCompactMulSupport f) (diff : ContMDiff I I' n f) :
    ContMDiff I I' n (Subtype.val.extend f 1) := fun x ↦ by
  refine contMDiff_of_mulTSupport (fun x h ↦ ?_) _
  lift x to U using Subtype.coe_image_subset _ _
    (supp.mulTSupport_extend_one_subset continuous_subtype_val h)
  rw [← contMDiffAt_subtype_iff]
  simp_rw [← comp_def]
  rw [extend_comp Subtype.val_injective]
  exact diff.contMDiffAt

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
E' : Type u_5
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H M
inst✝² : ChartedSpace H' M'
inst✝¹ : T2Space M
inst✝ : One M'
n : WithTop ℕ∞
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x : M
⊢ ContMDiffAt I I' n (extend Subtype.val f 1) x

Tactic:
refine contMDiff_of_mulTSupport (fun x h ↦ ?_) _

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
E' : Type u_5
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H M
inst✝² : ChartedSpace H' M'
inst✝¹ : T2Space M
inst✝ : One M'
n : WithTop ℕ∞
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ x : M
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n (extend Subtype.val f 1) x
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem Inseparable.nhds_le_uniformity {x y : α} (h : Inseparable x y) :
    𝓝 (x, y) ≤ 𝓤 α

Proof state:
α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (y, y) ≤ 𝓤 α

Tactic:
apply nhds_le_uniformity

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (x, y) ≤ 𝓤 α

Tactic:
rw [h.prod rfl]

Result:
α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (y, y) ≤ 𝓤 α
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
@[simp]
lemma mkOfHomEquiv_homEquiv (adj : CoreHomEquiv F G) :
    (mkOfHomEquiv adj).homEquiv = adj.homEquiv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ (mkOfHomEquiv adj).homEquiv = adj.homEquiv

Tactic:
ext X Y g

Result:
case h.h.H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
g : F.obj X ⟶ Y
⊢ ((mkOfHomEquiv adj).homEquiv X Y) g = (adj.homEquiv X Y) g

Proof state:
case h.h.H
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
g : F.obj X ⟶ Y
⊢ ((mkOfHomEquiv adj).homEquiv X Y) g = (adj.homEquiv X Y) g

Tactic:
simp [mkOfHomEquiv, ← adj.homEquiv_naturality_right (𝟙 _) g]

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
@[norm_cast]
lemma specializes_coe {f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
⊢ ⇑f ⤳ ⇑g ↔ f ⤳ g

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ f ⤳ g

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
this : ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen U → MapsTo (⇑g) K U → MapsTo (⇑f) K U
⊢ f ⤳ g

Tactic:
simpa [specializes_iff_pure, nhds_compactOpen]

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ f ⤳ g

Tactic:
suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
  simpa [specializes_iff_pure, nhds_compactOpen]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen U → MapsTo (⇑g) K U → MapsTo (⇑f) K U

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen U → MapsTo (⇑g) K U → MapsTo (⇑f) K U

Tactic:
exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem Cache.IsExtensionBy_rfl (cache : Cache aig cnf) {h} (hmarked : cache.marks[idx]'h = true) :
    Cache.IsExtensionBy cache cache idx (have := cache.hmarks; omega)

Proof state:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true

Tactic:
intros

Result:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
idx✝ : Nat
hidx✝ : idx✝ < aig.decls.size
a✝ : cache.marks[idx✝] = true
⊢ cache.marks[idx✝] = true

Proof state:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true

Tactic:
exact hmarked

Result:
no goals

Proof state:
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.IsExtensionBy cache idx ⋯

Tactic:
apply IsExtensionBy.mk

Result:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true

Proof state:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
idx✝ : Nat
hidx✝ : idx✝ < aig.decls.size
a✝ : cache.marks[idx✝] = true
⊢ cache.marks[idx✝] = true

Tactic:
assumption

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Functional equation for the even Hurwitz zeta function (alternative form). -/
lemma completedCosZeta_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedCosZeta a (1 - s) = completedHurwitzZetaEven a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta a (1 - s) = completedHurwitzZetaEven a s

Tactic:
rw [← completedHurwitzZetaEven_one_sub, sub_sub_cancel]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma evenKernel_def (a x : ℝ) :
    ↑(evenKernel ↑a x) = cexp (-π * a ^ 2 * x) * jacobiTheta₂ (a * I * x) (I * x)

Proof state:
a x : ℝ
⊢ ↑(evenKernel (↑a) x) = cexp (-↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)

Tactic:
simp [evenKernel, re_eq_add_conj, jacobiTheta₂_conj, ← mul_two,
  mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

Result:
no goals