harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
    {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) :
    ∫ v : EuclideanSpace ℝ ι, cexp (- b * ‖v‖^2 + c * ⟪w, v⟫) =
      (π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b))

Proof state:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm y)) = ∑ i : ι, c * ↑(w i) * ↑(y i)

Tactic:
simp [PiLp.inner_apply, EuclideanSpace.measurableEquiv, Finset.mul_sum, mul_assoc]

Result:
no goals

Proof state:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ -(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm y‖ ^ 2) = -b * ∑ i : ι, ↑(y i) ^ 2

Tactic:
simp only [EuclideanSpace.measurableEquiv, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
  EuclideanSpace.norm_eq, WithLp.equiv_symm_pi_apply, Real.norm_eq_abs, sq_abs, neg_mul,
  neg_inj, mul_eq_mul_left_iff]

Result:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ ↑√(∑ x : ι, y x ^ 2) ^ 2 = ∑ i : ι, ↑(y i) ^ 2 ∨ b = 0

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ∫ (x : ι → ℝ),
      cexp
        (-b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2 +
          c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm x))) ∂volume =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
simp only [neg_mul, Function.comp_def]

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ∫ (x : ι → ℝ),
      cexp
        (-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2) +
          c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm x))) ∂volume =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Proof state:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ c ^ 2 * ↑√(∑ x : ι, w x ^ 2) ^ 2 = c ^ 2 * ∑ i : ι, ↑(w i) ^ 2

Tactic:
congr

Result:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ↑√(∑ x : ι, w x ^ 2) ^ 2 = ∑ i : ι, ↑(w i) ^ 2
-- Mathlib/Data/Int/GCD.lean
theorem lcm_zero_left (i : ℤ) : lcm 0 i = 0

Proof state:
i : ℤ
⊢ lcm 0 i = 0

Tactic:
rw [Int.lcm]

Result:
i : ℤ
⊢ (natAbs 0).lcm i.natAbs = 0

Proof state:
i : ℤ
⊢ (natAbs 0).lcm i.natAbs = 0

Tactic:
apply Nat.lcm_zero_left

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem map_mk_disjoint_sym2 (x : α) (xs : List α) (h : x ∉ xs) :
    (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

Proof state:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ s(x', x') :: map (fun y => s(x', y)) xs ++ xs.sym2 ∧
    (s(x', x') ∉ map (fun y => s(x, y)) xs ∧ (map (fun y => s(x, y)) xs).Disjoint (map (fun y => s(x', y)) xs)) ∧
      (map (fun y => s(x, y)) xs).Disjoint xs.sym2

Tactic:
refine ⟨?_, ⟨?_, ?_⟩, ?_⟩

Result:
case cons.refine_1
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x, x') ∉ s(x', x') :: map (fun y => s(x', y)) xs ++ xs.sym2

case cons.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x', x') ∉ map (fun y => s(x, y)) xs

case cons.refine_3
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ (map (fun y => s(x, y)) xs).Disjoint (map (fun y => s(x', y)) xs)

case cons.refine_4
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ (map (fun y => s(x, y)) xs).Disjoint xs.sym2

Proof state:
case cons.refine_2
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
⊢ s(x', x') ∉ map (fun y => s(x, y)) xs

Tactic:
simp [h.1]

Result:
no goals

Proof state:
case cons.refine_3.intro.intro
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
a : α
hx : a ∈ xs
hy : ∃ a_1 ∈ xs, s(x', a_1) = s(x, a)
⊢ False

Tactic:
obtain ⟨b, hy, hx⟩ := hy

Result:
case cons.refine_3.intro.intro.intro.intro
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
a : α
hx✝ : a ∈ xs
b : α
hy : b ∈ xs
hx : s(x', b) = s(x, a)
⊢ False

Proof state:
case cons.refine_3.intro.intro.intro.intro
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y => s(x, y)) xs).Disjoint xs.sym2
h : ¬x = x' ∧ x ∉ xs
a : α
hx✝ : a ∈ xs
b : α
hy : b ∈ xs
hx : x' = a ∧ b = x
⊢ False

Tactic:
obtain ⟨rfl, rfl⟩ := hx

Result:
case cons.refine_3.intro.intro.intro.intro.intro
α : Type u_1
x' : α
xs : List α
b : α
hy : b ∈ xs
hx : x' ∈ xs
ih : b ∉ xs → (map (fun y => s(b, y)) xs).Disjoint xs.sym2
h : ¬b = x' ∧ b ∉ xs
⊢ False
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_singleton : 𝓝ˢ {x} = 𝓝 x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝ˢ {x} = 𝓝 x

Tactic:
simp [nhdsSet]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Perm.diff_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) : l₁.diff t ~ l₂.diff t

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ (if elem x l₁ = true then (l₁.erase x).diff t else l₁.diff t) ~
    if elem x l₂ = true then (l₂.erase x).diff t else l₂.diff t

Tactic:
simp only [elem_eq_mem, decide_eq_true_eq, Perm.mem_iff h]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ (if x ∈ l₂ then (l₁.erase x).diff t else l₁.diff t) ~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁ ~ l₂

Tactic:
exact h

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
h✝ : ¬x ∈ l₂
⊢ l₁.diff t ~ l₂.diff t

Tactic:
exact ih h

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ (if x ∈ l₂ then (l₁.erase x).diff t else l₁.diff t) ~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
h✝ : x ∈ l₂
⊢ (l₁.erase x).diff t ~ (l₂.erase x).diff t

case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
h✝ : ¬x ∈ l₂
⊢ l₁.diff t ~ l₂.diff t

Proof state:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.diff t ~ l₂.diff t
l₁ l₂ : List α
h : l₁ ~ l₂
h✝ : x ∈ l₂
⊢ (l₁.erase x).diff t ~ (l₂.erase x).diff t

Tactic:
exact ih (h.erase _)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three : W.j ≠ 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ W.j ≠ 0

Tactic:
rw [j_of_isCharThreeJNeZeroNF_of_char_three, div_ne_zero_iff]

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : ↑W.Δ' ≠ 0
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
rwa [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff] at h

Result:
no goals

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
have h := W.Δ'.ne_zero

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : ↑W.Δ' ≠ 0
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem exists_variableChange_isCharTwoNF :
    ∃ C : VariableChange F, (W.variableChange C).IsCharTwoNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
⊢ ∃ C, (W.variableChange C).IsCharTwoNF

Tactic:
classical
exact ⟨_, W.toCharTwoNF_spec⟩

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
⊢ ∃ C, (W.variableChange C).IsCharTwoNF

Tactic:
exact ⟨_, W.toCharTwoNF_spec⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : Vector α n) (init : β₁)
    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init)

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ foldr g₂ (f init) { toArray := toArray✝, size_toArray := size_toArray✝ } =
    f (foldr g₁ init { toArray := toArray✝, size_toArray := size_toArray✝ })

Tactic:
simp

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.foldr g₂ (f init) toArray✝ = f (Array.foldr g₁ init toArray✝)

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.foldr g₂ (f init) toArray✝ = f (Array.foldr g₁ init toArray✝)

Tactic:
rw [Array.foldr_hom _ _ _ _ _ H]

Result:
no goals

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
l : Vector α n
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
⊢ foldr g₂ (f init) l = f (foldr g₁ init l)

Tactic:
cases l

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ foldr g₂ (f init) { toArray := toArray✝, size_toArray := size_toArray✝ } =
    f (foldr g₁ init { toArray := toArray✝, size_toArray := size_toArray✝ })
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEmbedding_isBase_iff {f : α ↪ β} {B : Set β} :
    (M.mapEmbedding f).IsBase B ↔ M.IsBase (f ⁻¹' B) ∧ B ⊆ range f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (M.mapEmbedding f).IsBase B ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Tactic:
rw [mapEmbedding, map_isBase_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
x✝ : M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f
h : M.IsBase (⇑f ⁻¹' B)
h' : B ⊆ range ⇑f
⊢ B = ⇑f '' (⇑f ⁻¹' B)

Tactic:
rwa [eq_comm, image_preimage_eq_iff]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase (⇑f ⁻¹' (⇑f '' B)) ∧ ⇑f '' B ⊆ range ⇑f

Tactic:
rw [preimage_image_eq _ f.injective]

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase B ∧ ⇑f '' B ⊆ range ⇑f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase B ∧ ⇑f '' B ⊆ range ⇑f

Tactic:
exact ⟨hB, image_subset_range _ _⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' B, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) → M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) → M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Tactic:
rintro ⟨B, hB, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase (⇑f ⁻¹' (⇑f '' B)) ∧ ⇑f '' B ⊆ range ⇑f
-- Mathlib/ModelTheory/Equivalence.lean
lemma imp_inf {φ ψ θ : L.BoundedFormula α n} (h₁ : φ ⟹[T] ψ) (h₂ : φ ⟹[T] θ) :
    φ ⟹[T] ψ ⊓ θ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⟹ ψ ⊓ θ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs

Tactic:
exact fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.mem_nhds_iff_symm {x : α} {s : Set α} :
    s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Proof state:
case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
rintro ⟨V, V_in, _, V_sub⟩

Result:
case mpr.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left✝ : SymmetricRel V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
case mpr.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left✝ : SymmetricRel V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
exact ⟨V, V_in, V_sub⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Tactic:
rw [UniformSpace.mem_nhds_iff]

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Proof state:
case mp
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Tactic:
rintro ⟨V, V_in, V_sub⟩

Result:
case mp.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (symmetrizeRel V) ⊆ s

Tactic:
exact Subset.trans (ball_mono (symmetrizeRel_subset_self V) x) V_sub

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Tactic:
constructor

Result:
case mp
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
case mp.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s

Tactic:
use symmetrizeRel V, symmetrize_mem_uniformity V_in, symmetric_symmetrizeRel V

Result:
case right
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (symmetrizeRel V) ⊆ s
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_pow_le {f : MvPolynomial σ R} (n : ℕ) :
    m.degree (f ^ n) ≼[m] n • (m.degree f)

Proof state:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ (n + 1))) ≤ m.toSyn ((n + 1) • m.degree f)

Tactic:
simp only [pow_add, pow_one, add_smul, one_smul]

Result:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n * f)) ≤ m.toSyn (n • m.degree f + m.degree f)

Proof state:
case zero
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (f ^ 0)) ≤ m.toSyn (0 • m.degree f)

Tactic:
simp [m.degree_one]

Result:
no goals

Proof state:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n) + m.degree f) ≤ m.toSyn (n • m.degree f + m.degree f)

Tactic:
simp only [map_add, add_le_add_iff_right]

Result:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)

Proof state:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)

Tactic:
exact hrec

Result:
no goals

Proof state:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n * f)) ≤ m.toSyn (n • m.degree f + m.degree f)

Tactic:
apply le_trans m.degree_mul_le

Result:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n) + m.degree f) ≤ m.toSyn (n • m.degree f + m.degree f)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
⊢ m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)

Tactic:
induction n with
| zero => simp [m.degree_one]
| succ n hrec =>
    simp only [pow_add, pow_one, add_smul, one_smul]
    apply le_trans m.degree_mul_le
    simp only [map_add, add_le_add_iff_right]
    exact hrec

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem exists_subset_nhds_of_isCompact' [Nonempty ι] {V : ι → Set X}
    (hV : Directed (· ⊇ ·) V) (hV_cpct : ∀ i, IsCompact (V i)) (hV_closed : ∀ i, IsClosed (V i))
    {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U

Proof state:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 => x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
⊢ (⋂ i, V i ∩ Wᶜ).Nonempty

Tactic:
refine
  IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
    (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
    (hV_closed i).inter W_op.isClosed_compl

Result:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 => x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j : ι
⊢ ∃ z, (fun x1 x2 => x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x1 x2 => x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)

Proof state:
case intro.intro.intro
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 => x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this : (⋂ i, V i ∩ Wᶜ).Nonempty
⊢ False

Tactic:
have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]

Result:
case intro.intro.intro
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 => x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this✝ : (⋂ i, V i ∩ Wᶜ).Nonempty
this : ¬⋂ i, V i ⊆ W
⊢ False
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem toAddMonoid.unique (f : ⨁ i, β i) : ψ f = toAddMonoid (fun i => ψ.comp (of β i)) f

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ f = (toAddMonoid fun i => ψ.comp (of β i)) f

Tactic:
congr

Result:
case e_a
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ = toAddMonoid fun i => ψ.comp (of β i)

Proof state:
case e_a.H
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ∀ (x : ι),
    ψ.comp (DFinsupp.singleAddHom (fun i => β i) x) =
      (toAddMonoid fun i => ψ.comp (of β i)).comp (DFinsupp.singleAddHom (fun i => β i) x)

Tactic:
simp [toAddMonoid, of]

Result:
no goals

Proof state:
case e_a
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ = toAddMonoid fun i => ψ.comp (of β i)

Tactic:
apply DFinsupp.addHom_ext'

Result:
case e_a.H
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ∀ (x : ι),
    ψ.comp (DFinsupp.singleAddHom (fun i => β i) x) =
      (toAddMonoid fun i => ψ.comp (of β i)).comp (DFinsupp.singleAddHom (fun i => β i) x)
-- Mathlib/Data/Int/ModEq.lean
theorem sub (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a - c ≡ b - d [ZMOD n]

Proof state:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]

Tactic:
exact h₁.add h₂.neg

Result:
no goals

Proof state:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a - c ≡ b - d [ZMOD n]

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg]

Result:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]