harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem existsUnique_dist_eq_of_insert {s : AffineSubspace ℝ P}
    [HasOrthogonalProjection s.direction] {ps : Set P} (hnps : ps.Nonempty) {p : P} (hps : ps ⊆ s)
    (hp : p ∉ s) (hu : ∃! cs : Sphere P, cs.center ∈ s ∧ ps ⊆ (cs : Set P)) :
    ∃! cs₂ : Sphere P,
      cs₂.center ∈ affineSpan ℝ (insert p (s : Set P)) ∧ insert p ps ⊆ (cs₂ : Set P)

Proof state:
case h.left.right.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ = p
⊢ dist p { center := cc₂, radius := cr₂ }.center * dist p { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂

Tactic:
rw [hpo,
  dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc _ _
    (vsub_orthogonalProjection_mem_direction_orthogonal s p),
  ← dist_eq_norm_vsub V p, dist_comm _ cc]

Result:
case h.left.right.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ = p
⊢ dist cc ↑((orthogonalProjection s) p) * dist cc ↑((orthogonalProjection s) p) +
      (1 - ycc₂ / y) * (1 - ycc₂ / y) * (dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)) =
    cr * cr + ycc₂ * ycc₂
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.isLUB {c : Chain α} (hf : ωScottContinuous f) :
    IsLUB (Set.range (c.map ⟨f, hf.monotone⟩)) (f (ωSup c))

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ Set.range ⇑c ∈ Set.range fun c => Set.range ⇑c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (ωSup c))

Tactic:
simpa [map_coe, OrderHom.coe_mk, Set.range_comp]
  using hf (by simp) (Set.range_nonempty _) (isChain_range c).directedOn (isLUB_range_ωSup c)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_c₄ : (W.variableChange C).c₄ = C.u⁻¹ ^ 4 * W.c₄

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (W.variableChange C).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄

Tactic:
simp only [c₄, variableChange_b₂, variableChange_b₄]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 2 - 24 * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) =
    ↑C.u⁻¹ ^ 4 * (W.b₂ ^ 2 - 24 * W.b₄)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 2 - 24 * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) =
    ↑C.u⁻¹ ^ 4 * (W.b₂ ^ 2 - 24 * W.b₄)

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem get_eq_get_rotate (l : List α) (n : ℕ) (k : Fin l.length) :
    l.get k = (l.rotate n).get ⟨(l.length - n % l.length + k) % l.length,
      (Nat.mod_lt _ (k.1.zero_le.trans_lt k.2)).trans_eq (length_rotate _ _).symm⟩

Proof state:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = l.get ⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + n) % l.length, ⋯⟩

Tactic:
refine congr_arg l.get (Fin.eq_of_val_eq ?_)

Result:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ ↑k = ↑⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + n) % l.length, ⋯⟩

Proof state:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ ↑k = (l.length - n % l.length + ↑k + n) % l.length

Tactic:
rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]

Result:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ ↑k < l.length

α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ n % l.length ≤ l.length

Proof state:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩

Tactic:
rw [get_rotate]

Result:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = l.get ⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + n) % l.length, ⋯⟩

Proof state:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ ↑k = ↑⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + n) % l.length, ⋯⟩

Tactic:
simp only [mod_add_mod]

Result:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ ↑k = (l.length - n % l.length + ↑k + n) % l.length

Proof state:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ ↑k < l.length

α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ n % l.length ≤ l.length

Tactic:
exacts [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
theorem ZMod.erdos_ginzburg_ziv_prime (a : ι → ZMod p) (hs : #s = 2 * p - 1) :
    ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Proof state:
case intro.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s }
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ #(filter (fun a_1 => ↑x a_1 ≠ 0) univ) = p

Tactic:
refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
  (Finset.card_filter_le _ _).trans_lt ?_

Result:
case intro.refine_2.refine_1
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s }
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ (filter (fun a_1 => ↑x a_1 ≠ 0) univ).Nonempty

case intro.refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s }
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ p ∣ #(filter (fun a_1 => ↑x a_1 ≠ 0) univ)

case intro.refine_2.refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s }
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ #univ < 2 * p

Proof state:
case intro.refine_2.refine_1
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s }
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : ∃ a_1, ↑x a_1 ≠ ↑zero_sol a_1
⊢ (filter (fun a_1 => ↑x a_1 ≠ 0) univ).Nonempty

Tactic:
exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_eq_zero {n} :
    nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf : (setOf p).Finite, #hf.toFinset ≤ n

Proof state:
case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ n

Tactic:
simp only [or_iff_not_imp_right, not_exists, not_le]

Result:
case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ (∀ (x : (setOf p).Finite), n < #x.toFinset) → p 0 ∧ n = 0

Proof state:
case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ (∀ (x : (setOf p).Finite), n < #x.toFinset) → p 0 ∧ n = 0

Tactic:
exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩

Result:
no goals

Proof state:
p : ℕ → Prop
n : ℕ
⊢ nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ n

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

Result:
case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ n

case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Proof state:
case refine_2.inl.intro
p : ℕ → Prop
h₀ : p 0
⊢ nth p 0 = 0

case refine_2.inr.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hle : #hf.toFinset ≤ n
⊢ nth p n = 0

Tactic:
exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]

Result:
no goals

Proof state:
case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)

Result:
case refine_2.inl.intro
p : ℕ → Prop
h₀ : p 0
⊢ nth p 0 = 0

case refine_2.inr.intro
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hle : #hf.toFinset ≤ n
⊢ nth p n = 0
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem not_isUniform_zero : ¬G.IsUniform (0 : 𝕜) s t := fun h =>
  (abs_nonneg _).not_lt <| h (empty_subset _) (empty_subset _) (by simp) (by simp)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
h : G.IsUniform 0 s t
⊢ ↑(#s) * 0 ≤ ↑(#∅)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
h : G.IsUniform 0 s t
⊢ ↑(#t) * 0 ≤ ↑(#∅)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem constantCoeff_wittNeg (n : ℕ) : constantCoeff (wittNeg p n) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittNeg p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (-X 0) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (-X 0) = 0

Tactic:
simp only [neg_zero, RingHom.map_neg, constantCoeff_X]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem mk_toNat_of_infinite [h : Infinite α] : toNat #α = 0

Proof state:
α : Type u
h : Infinite α
⊢ toNat #α = 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem MeasurableEmbedding.essSup_map_measure (hf : MeasurableEmbedding f) :
    essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ essSup g (Measure.map f μ) ≤ essSup (g ∘ f) μ

Tactic:
refine limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_le => ?_)

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf.measurable.aemeasurable)

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ essSup g (Measure.map f μ) ≤ essSup (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ IsBounded (fun x1 x2 => x1 ≤ x2) (map (g ∘ f) (ae μ))

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c

Tactic:
rw [eventually_map] at h_le ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ IsCobounded (fun x1 x2 => x1 ≤ x2) (map g (ae (Measure.map f μ)))

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c

Tactic:
exact hf.ae_map_iff.mpr h_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
    (some l[i] = l[i]?) ↔ True

Proof state:
w : Nat
l : BitVec w
i : Nat
h : i < w
⊢ some l[i] = l[i]? ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Seq/Parallel.lean
theorem terminates_parallel.aux :
    ∀ {l : List (Computation α)} {S c},
      c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S))

Proof state:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, c ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
apply @terminatesRecOn _ _ c T _ _

Result:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
⊢ ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
⊢ ∀ (s : Computation α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Proof state:
case cons.inr.inr.inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) c.destruct)
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
val✝ : Computation α
h' : val✝ :: ls = l'
⊢ s ∈ val✝ :: ls

Tactic:
simp [this]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma continuous_bool_rng [TopologicalSpace X] {f : X → Bool} (b : Bool) :
    Continuous f ↔ IsClopen (f ⁻¹' {b})

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ Continuous f ↔ IsClopen (f ⁻¹' {b})

Tactic:
rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
  Bool.compl_singleton, and_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- A polynomial sequence spans `R[X]` if all of its elements' leading coefficients are units. -/
protected lemma span (hCoeff : ∀ i, IsUnit (S i).leadingCoeff) : span R (Set.range S) = ⊤

Proof state:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
u : R
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
p_ne_zero : ¬P = 0
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
tail_eq_zero : ¬tail = 0
head_degree_eq : P.natDegree = head.natDegree
⊢ P.leadingCoeff = (P.leadingCoeff • u • ↑S n).coeff (↑S n).natDegree

R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
⊢ P ≠ 0

Tactic:
rwa [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
⊢ head ∈ span R (Set.range ↑S)

Tactic:
have in_span : S n ∈ span R (Set.range S) := subset_span (by simp)

Result:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
in_span : ↑S n ∈ span R (Set.range ↑S)
⊢ head ∈ span R (Set.range ↑S)
-- Mathlib/Data/List/Prime.lean
theorem mem_list_primes_of_dvd_prod {p : M} (hp : Prime p) {L : List M} (hL : ∀ q ∈ L, Prime q)
    (hpL : p ∣ L.prod) : p ∈ L

Proof state:
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ q ∈ L, Prime q
hpL : p ∣ L.prod
⊢ p ∈ L

Tactic:
obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL

Result:
case intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ q ∈ L, Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L

Proof state:
case intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ q ∈ L, Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L

Tactic:
rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem inf_comap_le_comap_add (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) :
    comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ f₁ m + f₂ m ∈ q

Tactic:
change f₁ m ∈ q ∧ f₂ m ∈ q at h

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : f₁ m ∈ q ∧ f₂ m ∈ q
⊢ f₁ m + f₂ m ∈ q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ m ∈ comap (f₁ + f₂) q

Tactic:
change f₁ m + f₂ m ∈ q

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ f₁ m + f₂ m ∈ q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q

Tactic:
rw [SetLike.le_def]

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄, x ∈ comap f₁ q ⊓ comap f₂ q → x ∈ comap (f₁ + f₂) q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄, x ∈ comap f₁ q ⊓ comap f₂ q → x ∈ comap (f₁ + f₂) q

Tactic:
intro m h

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ m ∈ comap (f₁ + f₂) q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : f₁ m ∈ q ∧ f₂ m ∈ q
⊢ f₁ m + f₂ m ∈ q

Tactic:
apply q.add_mem h.1 h.2

Result:
no goals