harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_sup_eq {K₀ : PositiveCompacts G} {U : Set G} {K₁ K₂ : Compacts G}
    (hU : (interior U).Nonempty) (h : Disjoint (K₁.1 * U⁻¹) (K₂.1 * U⁻¹)) :
    prehaar (K₀ : Set G) U (K₁ ⊔ K₂) = prehaar (K₀ : Set G) U K₁ + prehaar (K₀ : Set G) U K₂

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ prehaar (↑K₀) U (K₁ ⊔ K₂) = prehaar (↑K₀) U K₁ + prehaar (↑K₀) U K₂

Tactic:
simp only [prehaar]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
rw [div_add_div_same]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = (↑(index (↑K₁) U) + ↑(index (↑K₂) U)) / ↑(index (↑K₀) U)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = (↑(index (↑K₁) U) + ↑(index (↑K₂) U)) / ↑(index (↑K₀) U)

Tactic:
refine congr_arg (fun x : ℝ => x / index K₀ U) ?_

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) = ↑(index (↑K₁) U) + ↑(index (↑K₂) U)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) = ↑(index (↑K₁) U) + ↑(index (↑K₂) U)

Tactic:
exact mod_cast index_union_eq K₁ K₂ hU h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
@[simp] lemma replaceVertex_self : G.replaceVertex s s = G

Proof state:
case Adj.h.h.a
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ { Adj := fun v w => if v = s then if w = s then False else G.Adj s w else if w = s then G.Adj v s else G.Adj v w,
          symm := ⋯, loopless := ⋯ }.Adj
      x✝¹ x✝ ↔
    G.Adj x✝¹ x✝

Tactic:
aesop (add simp or_iff_not_imp_left)

Result:
no goals

Proof state:
case Adj.h.h.a
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ (G.replaceVertex s s).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
unfold replaceVertex

Result:
case Adj.h.h.a
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ { Adj := fun v w => if v = s then if w = s then False else G.Adj s w else if w = s then G.Adj v s else G.Adj v w,
          symm := ⋯, loopless := ⋯ }.Adj
      x✝¹ x✝ ↔
    G.Adj x✝¹ x✝

Proof state:
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
⊢ G.replaceVertex s s = G

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ (G.replaceVertex s s).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_rpow_left_iff (hx : 1 < x) : x ^ y < x ^ z ↔ y < z

Proof state:
x y z : ℝ
hx : 1 < x
⊢ x ^ y < x ^ z ↔ y < z

Tactic:
rw [lt_iff_not_le, rpow_le_rpow_left_iff hx, lt_iff_not_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
    elem a l = l.contains a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ elem a l = l.contains a

Tactic:
simp [contains]

Result:
no goals
-- Mathlib/Topology/Instances/Nat.lean
theorem closedBall_eq_Icc (x : ℕ) (r : ℝ) : closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Proof state:
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r

Tactic:
linarith

Result:
no goals

Proof state:
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x + r ≤ ↑x

Tactic:
linarith

Result:
no goals

Proof state:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊

Tactic:
calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
_ < ⌈↑x - r⌉₊ := by
  rw [floor_natCast, Nat.lt_ceil]
  linarith

Result:
no goals

Proof state:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r

Tactic:
exact add_nonneg (cast_nonneg x) hr

Result:
no goals

Proof state:
x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
rcases le_or_lt 0 r with (hr | hr)

Result:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Proof state:
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊

Tactic:
rw [floor_natCast, Nat.lt_ceil]

Result:
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r

Proof state:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

Result:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r

Proof state:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]

Result:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem ext_iff_natDegree_le {p q : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) :
    p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
⊢ p.coeff i = q.coeff i

Tactic:
refine (le_or_lt i n).elim h fun k => ?_

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
k : n < i
⊢ p.coeff i = q.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
refine Iff.trans Polynomial.ext_iff ?_

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
k : n < i
⊢ p.coeff i = q.coeff i

Tactic:
exact
  (coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans
    (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
refine forall_congr' fun i => ⟨fun h _ => h, fun h => ?_⟩

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
⊢ p.coeff i = q.coeff i
-- Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean
/-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
of `s`, and over all subsets of `s` to which one adds `x`. -/
@[to_additive "A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all subsets
of `s`, and over all subsets of `s` to which one adds `x`."]
lemma prod_powerset_cons (ha : a ∉ s) (f : Finset α → β) :
    ∏ t ∈ (s.cons a ha).powerset, f t = (∏ t ∈ s.powerset, f t) *
      ∏ t ∈ s.powerset.attach, f (cons a t <| not_mem_mono (mem_powerset.1 t.2) ha)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

Tactic:
classical
simp_rw [cons_eq_insert]
rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

Tactic:
simp_rw [cons_eq_insert]

Result:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ x ∈ (insert a s).powerset, f x = (∏ x ∈ s.powerset, f x) * ∏ x ∈ s.powerset.attach, f (insert a ↑x)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ x ∈ (insert a s).powerset, f x = (∏ x ∈ s.powerset, f x) * ∏ x ∈ s.powerset.attach, f (insert a ↑x)

Tactic:
rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrable_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (support g))
    (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Proof state:
case refine_2
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable ((support g).indicator (f + g)) μ

Tactic:
exact hfg.indicator hg.measurableSet_support

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩

Result:
case refine_1
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable f μ

case refine_2
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable g μ

Proof state:
case refine_1
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable ((support f).indicator (f + g)) μ

Tactic:
exact hfg.indicator hf.measurableSet_support

Result:
no goals

Proof state:
case refine_2
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable g μ

Tactic:
rw [← indicator_add_eq_right h]

Result:
case refine_2
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable ((support g).indicator (f + g)) μ

Proof state:
case refine_1
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable f μ

Tactic:
rw [← indicator_add_eq_left h]

Result:
case refine_1
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable ((support f).indicator (f + g)) μ
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCommutative] :
    (H.comap f).IsCommutative :=
  ⟨⟨fun a b =>
      Subtype.ext
        (by
          have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)
          rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul,
            hf.eq_iff] at this)⟩⟩

Proof state:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : H.IsCommutative
a b : ↥(comap f H)
this : ⟨f ↑a, ⋯⟩ * ⟨f ↑b, ⋯⟩ = ⟨f ↑b, ⋯⟩ * ⟨f ↑a, ⋯⟩
⊢ ↑(a * b) = ↑(b * a)

Tactic:
rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul,
  hf.eq_iff] at this

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : H.IsCommutative
a b : ↥(comap f H)
⊢ ↑(a * b) = ↑(b * a)

Tactic:
have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)

Result:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : H.IsCommutative
a b : ↥(comap f H)
this : ⟨f ↑a, ⋯⟩ * ⟨f ↑b, ⋯⟩ = ⟨f ↑b, ⋯⟩ * ⟨f ↑a, ⋯⟩
⊢ ↑(a * b) = ↑(b * a)
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getVert_mem_support {u v : V} (p : G.Walk u v) (i : ℕ) : p.getVert i ∈ p.support

Proof state:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
hind : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
n✝ : ℕ
⊢ (cons h✝ p✝).getVert (n✝ + 1) ∈ (cons h✝ p✝).support

Tactic:
simp [hind]

Result:
no goals

Proof state:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
hind : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
⊢ (cons h✝ p✝).getVert 0 ∈ (cons h✝ p✝).support

Tactic:
simp

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
⊢ nil.getVert i ∈ nil.support

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
hind : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
i : ℕ
⊢ (cons h✝ p✝).getVert i ∈ (cons h✝ p✝).support

Tactic:
cases i

Result:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
hind : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
⊢ (cons h✝ p✝).getVert 0 ∈ (cons h✝ p✝).support

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
hind : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
n✝ : ℕ
⊢ (cons h✝ p✝).getVert (n✝ + 1) ∈ (cons h✝ p✝).support
-- Mathlib/Computability/EpsilonNFA.lean
theorem mem_εClosure_iff_exists : s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} where
  mp h

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
h : s ∈ M.εClosure {t}
⊢ s ∈ M.εClosure S

Tactic:
induction' h <;> subst_vars <;> solve_by_elim [εClosure.step]

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
h : s ∈ M.εClosure S
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}

Tactic:
induction' h with s _ _ _ _ _ ih

Result:
case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s✝ s : σ
a✝ : s ∈ S
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}

case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
ih : ∃ t ∈ S, s✝ ∈ M.εClosure {t}
⊢ ∃ t ∈ S, t✝ ∈ M.εClosure {t}

Proof state:
case step.intro.intro
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s✝¹ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
s : σ
left✝ : s ∈ S
right✝ : s✝ ∈ M.εClosure {s}
⊢ ∃ t ∈ S, t✝ ∈ M.εClosure {t}

Tactic:
use s

Result:
case h
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s✝¹ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
s : σ
left✝ : s ∈ S
right✝ : s✝ ∈ M.εClosure {s}
⊢ s ∈ S ∧ t✝ ∈ M.εClosure {s}

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ (∃ t ∈ S, s ∈ M.εClosure {t}) → s ∈ M.εClosure S

Tactic:
intro ⟨t, _, h⟩

Result:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left✝ : t ∈ S
h : s ∈ M.εClosure {t}
⊢ s ∈ M.εClosure S

Proof state:
case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
ih : ∃ t ∈ S, s✝ ∈ M.εClosure {t}
⊢ ∃ t ∈ S, t✝ ∈ M.εClosure {t}

Tactic:
obtain ⟨s, _, _⟩ := ih

Result:
case step.intro.intro
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s✝¹ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
s : σ
left✝ : s ∈ S
right✝ : s✝ ∈ M.εClosure {s}
⊢ ∃ t ∈ S, t✝ ∈ M.εClosure {t}

Proof state:
case h
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s✝¹ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
s : σ
left✝ : s ∈ S
right✝ : s✝ ∈ M.εClosure {s}
⊢ s ∈ S ∧ t✝ ∈ M.εClosure {s}

Tactic:
solve_by_elim [εClosure.step]

Result:
no goals

Proof state:
case base
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s✝ s : σ
a✝ : s ∈ S
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Ring/Identities.lean
theorem sq_add_sq_mul_sq_add_sq :
    (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2

Proof state:
R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ : R
⊢ (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
lemma star_mul_self_add_self_mul_star {A : Type*} [NonUnitalRing A] [StarRing A]
    [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (a : A) :
    star a * a + a * star a = 2 • (ℜ a * ℜ a + ℑ a * ℑ a) :=
  have a_eq := (realPart_add_I_smul_imaginaryPart a).symm
  calc
    star a * a + a * star a = _ :=
      congr((star $(a_eq)) * $(a_eq) + $(a_eq) * (star $(a_eq)))
    _ = 2 • (ℜ a * ℜ a + ℑ a * ℑ a)

Proof state:
A : Type u_2
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) + (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) =
    2 • (↑(ℜ a) * ↑(ℜ a) + ↑(ℑ a) * ↑(ℑ a))

Tactic:
simp [mul_add, add_mul, smul_smul, two_smul, mul_smul_comm,
  smul_mul_assoc]

Result:
A : Type u_2
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ ↑(ℜ a) * ↑(ℜ a) + -(I • (↑(ℑ a) * ↑(ℜ a))) + (I • (↑(ℜ a) * ↑(ℑ a)) + ↑(ℑ a) * ↑(ℑ a)) +
      (↑(ℜ a) * ↑(ℜ a) + I • (↑(ℑ a) * ↑(ℜ a)) + (↑(ℑ a) * ↑(ℑ a) + -(I • (↑(ℜ a) * ↑(ℑ a))))) =
    ↑(ℜ a) * ↑(ℜ a) + ↑(ℜ a) * ↑(ℜ a) + (↑(ℑ a) * ↑(ℑ a) + ↑(ℑ a) * ↑(ℑ a))

Proof state:
A : Type u_2
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ ↑(ℜ a) * ↑(ℜ a) + -(I • (↑(ℑ a) * ↑(ℜ a))) + (I • (↑(ℜ a) * ↑(ℑ a)) + ↑(ℑ a) * ↑(ℑ a)) +
      (↑(ℜ a) * ↑(ℜ a) + I • (↑(ℑ a) * ↑(ℜ a)) + (↑(ℑ a) * ↑(ℑ a) + -(I • (↑(ℜ a) * ↑(ℑ a))))) =
    ↑(ℜ a) * ↑(ℜ a) + ↑(ℜ a) * ↑(ℜ a) + (↑(ℑ a) * ↑(ℑ a) + ↑(ℑ a) * ↑(ℑ a))

Tactic:
abel

Result:
no goals
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The set we are interested in (prime numbers in the residue class `a`) is the same as the support
of `ArithmeticFunction.vonMangoldt.residueClass` restricted to primes (and divided by `n`;
this is how this result is used later). -/
lemma support_residueClass_prime_div :
    Function.support (fun n : ℕ ↦ (if n.Prime then residueClass a n else 0) / n) =
      {p : ℕ | p.Prime ∧ (p : ZMod q) = a}

Proof state:
case h
q : ℕ
a : ZMod q
p : ℕ
⊢ (Nat.Prime p ∧ ↑p = a ∧ ¬Λ p = 0) ∧ ¬p = 0 ↔ Nat.Prime p ∧ ↑p = a

Tactic:
exact ⟨fun H ↦ ⟨H.1.1, H.1.2.1⟩,
  fun H ↦ ⟨⟨H.1, H.2, vonMangoldt_ne_zero_iff.mpr H.1.isPrimePow⟩, H.1.ne_zero⟩⟩

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
⊢ (Function.support fun n => (if Nat.Prime n then residueClass a n else 0) / ↑n) = {p | Nat.Prime p ∧ ↑p = a}

Tactic:
simp only [Function.support, ne_eq, div_eq_zero_iff, ite_eq_right_iff,
  Set.indicator_apply_eq_zero, Set.mem_setOf_eq, Nat.cast_eq_zero, not_or, Classical.not_imp]

Result:
q : ℕ
a : ZMod q
⊢ {x | (Nat.Prime x ∧ ↑x = a ∧ ¬Λ x = 0) ∧ ¬x = 0} = {p | Nat.Prime p ∧ ↑p = a}

Proof state:
case h
q : ℕ
a : ZMod q
p : ℕ
⊢ p ∈ {x | (Nat.Prime x ∧ ↑x = a ∧ ¬Λ x = 0) ∧ ¬x = 0} ↔ p ∈ {p | Nat.Prime p ∧ ↑p = a}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
case h
q : ℕ
a : ZMod q
p : ℕ
⊢ (Nat.Prime p ∧ ↑p = a ∧ ¬Λ p = 0) ∧ ¬p = 0 ↔ Nat.Prime p ∧ ↑p = a

Proof state:
q : ℕ
a : ZMod q
⊢ {x | (Nat.Prime x ∧ ↑x = a ∧ ¬Λ x = 0) ∧ ¬x = 0} = {p | Nat.Prime p ∧ ↑p = a}

Tactic:
ext1 p

Result:
case h
q : ℕ
a : ZMod q
p : ℕ
⊢ p ∈ {x | (Nat.Prime x ∧ ↑x = a ∧ ¬Λ x = 0) ∧ ¬x = 0} ↔ p ∈ {p | Nat.Prime p ∧ ↑p = a}
-- Mathlib/NumberTheory/Pell.lean
theorem y_le_y {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x)
    (hay : 0 < a.y) : a₁.y ≤ a.y

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ≤ a.x

Tactic:
exact h.x_le_x hax

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.y ≤ a.y

Tactic:
rw [← abs_of_pos hay, ← abs_of_pos h.2.1, ← sq_le_sq, ← mul_le_mul_left h.d_pos, ← sub_nonpos, ←
  mul_sub, H, sub_nonpos, sq_le_sq, abs_of_pos (zero_lt_one.trans h.1),
  abs_of_pos (zero_lt_one.trans hax)]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ≤ a.x

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2

Tactic:
rw [a.prop_x, a₁.prop_x]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = 1 + d * a₁.y ^ 2 - (1 + d * a.y ^ 2)

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = 1 + d * a₁.y ^ 2 - (1 + d * a.y ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y

Tactic:
have H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2 := by rw [a.prop_x, a₁.prop_x]; ring

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.y ≤ a.y
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_assoc (x y z : α) : (x ⊓ y) \ z = x ⊓ y \ z :=
  sdiff_unique
    (calc
      x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z

Tactic:
rw [inf_assoc]

Result:
no goals

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥

Tactic:
rw [inf_inf_sdiff, inf_bot_eq]

Result:
no goals

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ y ⊓ z ⊓ (x ⊓ y \ z) = x ⊓ x ⊓ (y ⊓ z ⊓ y \ z)

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y

Tactic:
rw [sup_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z ⊔ y \ z)

Tactic:
rw [← inf_sup_left]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_sUnion_left (S : Set (Set α)) (t : Set β) :
    image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

Tactic:
aesop

Result:
no goals