harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_affineCombinationLineMapWeights [DecidableEq ι] {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
    (c : k) : ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ x ∈ s, (c • weightedVSubVSubWeights k j i) x + ∑ x ∈ s, affineCombinationSingleWeights k i x = 1

Tactic:
simp [hi, hj, ← mul_sum]

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1

Tactic:
simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]

Result:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ x ∈ s, (c • weightedVSubVSubWeights k j i) x + ∑ x ∈ s, affineCombinationSingleWeights k i x = 1
-- Mathlib/Topology/Homeomorph.lean
@[continuity, fun_prop]
lemma continuous_sumAssoc : Continuous (Equiv.sumAssoc X Y Z) :=
  Continuous.sumElim (by fun_prop) (by fun_prop)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous (Sum.inr ∘ Sum.inr)

Tactic:
fun_prop

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl))

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem extend_injective (hf : Injective f) (e' : β → γ) : Injective fun g ↦ extend f g e'

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x

Tactic:
exact H

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
⊢ g₁ = g₂

Tactic:
refine funext fun x ↦ ?_

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
⊢ g₁ x = g₂ x

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
⊢ Injective fun g => extend f g e'

Tactic:
intro g₁ g₂ hg

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
⊢ g₁ = g₂

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : (fun g => extend f g e') g₁ (f x) = (fun g => extend f g e') g₂ (f x)
⊢ g₁ x = g₂ x

Tactic:
simp only [hf.extend_apply] at H

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
⊢ g₁ x = g₂ x

Tactic:
have H := congr_fun hg (f x)

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g => extend f g e') g₁ = (fun g => extend f g e') g₂
x : α
H : (fun g => extend f g e') g₁ (f x) = (fun g => extend f g e') g₂ (f x)
⊢ g₁ x = g₂ x
-- Mathlib/Data/Finmap.lean
theorem empty_union {s₁ : Finmap β} : ∅ ∪ s₁ = s₁ :=
  induction_on s₁ fun s₁ => by
    rw [← empty_toFinmap]
    simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧

Tactic:
simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ∅ ∪ ⟦s₁⟧ = ⟦s₁⟧

Tactic:
rw [← empty_toFinmap]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_zero : ~~~(0#n) = allOnes n

Proof state:
case pred
n i✝ : Nat
a✝ : i✝ < n
⊢ (~~~0#n).getLsbD i✝ = (allOnes n).getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ ~~~0#n = allOnes n

Tactic:
ext

Result:
case pred
n i✝ : Nat
a✝ : i✝ < n
⊢ (~~~0#n).getLsbD i✝ = (allOnes n).getLsbD i✝
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc]
lemma ιTensorObj₃_eq (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) :
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
      (X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h') ≫
        ιTensorObj X₁ (tensorObj X₂ X₃) i₁ i₂₃ j (by rw [← h', ← add_assoc, h])

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ ιTensorObj X₁ (tensorObj X₂ X₃) i₁ (i₂ + i₃) j ⋯

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h' ≫ ιTensorObj X₁ (tensorObj X₂ X₃) i₁ i₂₃ j ⋯

Tactic:
subst h'

Result:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ ιTensorObj X₁ (tensorObj X₂ X₃) i₁ (i₂ + i₃) j ⋯

Proof state:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{?u.68538, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + i₂₃ = j

Tactic:
rw [← h', ← add_assoc, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem comap_leq_ker_subToSupQuotient (p p' : Submodule R M) :
    comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p')

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap p.subtype (p ⊓ p') ≤ ker (subToSupQuotient p p')

Tactic:
rw [LinearMap.ker_comp, Submodule.inclusion, comap_codRestrict, ker_mkQ, map_comap_subtype]

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap p.subtype (p ⊓ p') ≤ comap p.subtype ((p ⊔ p') ⊓ p')

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap p.subtype (p ⊓ p') ≤ comap p.subtype ((p ⊔ p') ⊓ p')

Tactic:
exact comap_mono (inf_le_inf_right _ le_sup_left)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_or_inj_right : ∀ {m x y : Bool}, (x && m) = (y && m) → (x || m) = (y || m) → x = y

Proof state:
⊢ ∀ {m x y : Bool}, (x && m) = (y && m) → (x || m) = (y || m) → x = y

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.prod_map {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'}
    {f' : α' → β'} {q : Filter ι'} {q' : Filter α'} (h : TendstoUniformlyOnFilter F f p p')
    (h' : TendstoUniformlyOnFilter F' f' q q') :
    TendstoUniformlyOnFilter (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (Prod.map f f')
      (p ×ˢ q) (p' ×ˢ q')

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
⊢ TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q => (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q') (𝓤 (β × β'))

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun q => (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ∘
      fun p => ((p.1.1, p.2.1), p.1.2, p.2.2))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')

Tactic:
convert h.prod_map h'

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q => (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q') (𝓤 (β × β'))

Tactic:
rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun q => (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ∘
      fun p => ((p.1.1, p.2.1), p.1.2, p.2.2))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H} {a} (h : a ∈ l) :
    f a (H a h) ∈ pmap f l H

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ f a ⋯ ∈ pmap f l H

Tactic:
rw [mem_pmap]

Result:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ ∃ a_1 h_1, f a_1 ⋯ = f a ⋯

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ ∃ a_1 h_1, f a_1 ⋯ = f a ⋯

Tactic:
exact ⟨a, h, rfl⟩

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
/-- A measurable function `α → StieltjesFunction` with limits 0 at -∞ and 1 at +∞ gives a measurable
function `α → Measure ℝ` by taking `StieltjesFunction.measure` at each point. -/
lemma StieltjesFunction.measurable_measure {α : Type*} {_ : MeasurableSpace α}
    {f : α → StieltjesFunction} (hf : ∀ q, Measurable fun a ↦ f a q)
    (hf_bot : ∀ a, Tendsto (f a) atBot (𝓝 0))
    (hf_top : ∀ a, Tendsto (f a) atTop (𝓝 1)) :
    Measurable fun a ↦ (f a).measure :=
  have : ∀ a, IsProbabilityMeasure (f a).measure :=
    fun a ↦ (f a).isProbabilityMeasure (hf_bot a) (hf_top a)
  .measure_of_isPiSystem_of_isProbabilityMeasure (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic <| by
    simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]
    exact fun _ ↦ (hf _).ennreal_ofReal

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction
hf : ∀ (q : ℝ), Measurable fun a => ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ (i : ℝ), Measurable fun a => ENNReal.ofReal (↑(f a) i)

Tactic:
exact fun _ ↦ (hf _).ennreal_ofReal

Result:
no goals

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction
hf : ∀ (q : ℝ), Measurable fun a => ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ s ∈ range Iic, Measurable fun a => (f a).measure s

Tactic:
simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]

Result:
α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction
hf : ∀ (q : ℝ), Measurable fun a => ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ (i : ℝ), Measurable fun a => ENNReal.ofReal (↑(f a) i)
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveLeft_neg {x : PGame} (i) :
    (-x).moveLeft i = -x.moveRight (toLeftMovesNeg.symm i)

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (-mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (-mk α✝ β✝ a✝¹ a✝).moveLeft i = -(mk α✝ β✝ a✝¹ a✝).moveRight (toLeftMovesNeg.symm i)

Tactic:
rfl

Result:
no goals

Proof state:
x : PGame
i : (-x).LeftMoves
⊢ (-x).moveLeft i = -x.moveRight (toLeftMovesNeg.symm i)

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (-mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (-mk α✝ β✝ a✝¹ a✝).moveLeft i = -(mk α✝ β✝ a✝¹ a✝).moveRight (toLeftMovesNeg.symm i)
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.of_append_right {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
    (h : (p.append q).IsTrail) : q.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).IsTrail
⊢ q.IsTrail

Tactic:
rw [isTrail_def, edges_append, List.nodup_append] at h

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ p.edges.Disjoint q.edges
⊢ q.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ p.edges.Disjoint q.edges
⊢ q.IsTrail

Tactic:
exact ⟨h.2.1⟩

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.pair_iff {x y : R} :
    CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
⊢ x * (1 - x) = 0 ∧ (1 - x) * x = 0 ↔ IsIdempotentElem x

Tactic:
simp [mul_sub, sub_mul, IsIdempotentElem, sub_eq_zero, eq_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
⊢ y = 1 - x → (x * y = 0 ∧ y * x = 0 ↔ IsIdempotentElem x)

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝ : Ring R
x : R
⊢ x * (1 - x) = 0 ∧ (1 - x) * x = 0 ↔ IsIdempotentElem x

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x

Tactic:
rw [pair_iff'ₛ, ← eq_sub_iff_add_eq', ← and_assoc, and_congr_left_iff]

Result:
R : Type u_1
inst✝ : Ring R
x y : R
⊢ y = 1 - x → (x * y = 0 ∧ y * x = 0 ↔ IsIdempotentElem x)
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_nhds_of_re_neg_of_im_neg (hx_re : x.re < 0) (hx_im : x.im < 0) :
    arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) - π

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0

Tactic:
refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)

Result:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ IsOpen fun y => y.re < 0 ∧ y.im < 0

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ IsOpen fun y => y.re < 0 ∧ y.im < 0

Tactic:
exact
  IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)

Result:
no goals

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) - π

Tactic:
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ y.im < 0 from
  h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_neg hy.1 hy.2

Result:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_curry₃ {γ : Type*} (f : α × β × γ → M) (h : (mulSupport f).Finite) :
    ∏ᶠ abc, f abc = ∏ᶠ (a) (b) (c), f (a, b, c)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
⊢ ∏ᶠ (a : α) (b : β × γ), f (a, b) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
⊢ (fun a => ∏ᶠ (b : β × γ), f (a, b)) = fun a => ∏ᶠ (b : β) (c : γ), f (a, b, c)

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
a : α
⊢ ∏ᶠ (b : β × γ), f (a, b) = ∏ᶠ (b : β) (c : γ), f (a, b, c)

Tactic:
rw [finprod_curry]

Result:
case e_f.h.hf
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
a : α
⊢ (mulSupport fun b => f (a, b)).Finite

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
⊢ ∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)

Tactic:
rw [finprod_curry f h]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
⊢ ∏ᶠ (a : α) (b : β × γ), f (a, b) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)

Proof state:
case e_f.h.hf
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
a : α
⊢ (mulSupport fun b => f (a, b)).Finite

Tactic:
simp [h]

Result:
no goals

Proof state:
case e_f
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
⊢ (fun a => ∏ᶠ (b : β × γ), f (a, b)) = fun a => ∏ᶠ (b : β) (c : γ), f (a, b, c)

Tactic:
ext a

Result:
case e_f.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : (mulSupport f).Finite
a : α
⊢ ∏ᶠ (b : β × γ), f (a, b) = ∏ᶠ (b : β) (c : γ), f (a, b, c)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_eq_false_of_le (u v k : Nat) : isLt 0 k = true → u ≤ v → (v + k ≤ u) = False

Proof state:
u v k : Nat
⊢ isLt 0 k = true → u ≤ v → (v + k ≤ u) = False

Tactic:
simp [isLt]

Result:
u v k : Nat
⊢ 0 < k → u ≤ v → u < v + k

Proof state:
u v k : Nat
⊢ 0 < k → u ≤ v → u < v + k

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
theorem abs_geomSum_le : |geomSum a b n| ≤ (n + 1) * max |a| |b| ^ n

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, mul_comm |a|]

Result:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |geomSum a b n| * |a| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n * (|a| ⊔ |b|)

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ (↑n + 1) * (|a| ⊔ |b|) ^ (n + 1) + (|a| ⊔ |b|) ^ (n + 1)

Tactic:
refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)

Result:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ (n + 1)

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |a * geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * (|a| ⊔ |b|) ^ (n + 1)

Tactic:
rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]

Result:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ (↑n + 1) * (|a| ⊔ |b|) ^ (n + 1) + (|a| ⊔ |b|) ^ (n + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |geomSum a b 0| ≤ (↑0 + 1) * (|a| ⊔ |b|) ^ 0

case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |geomSum a b (n + 1)| ≤ (↑(n + 1) + 1) * (|a| ⊔ |b|) ^ (n + 1)

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |geomSum a b n| * |a| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n * (|a| ⊔ |b|)

Tactic:
exact mul_le_mul ih le_sup_left (abs_nonneg _) (mul_nonneg
  (@Nat.cast_succ α .. ▸ Nat.cast_nonneg _) <| pow_nonneg ((abs_nonneg _).trans le_sup_left) _)

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |geomSum a b (n + 1)| ≤ (↑(n + 1) + 1) * (|a| ⊔ |b|) ^ (n + 1)

Tactic:
refine (abs_add_le ..).trans ?_

Result:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * (|a| ⊔ |b|) ^ n
⊢ |a * geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * (|a| ⊔ |b|) ^ (n + 1)

Proof state:
case zero
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |geomSum a b 0| ≤ (↑0 + 1) * (|a| ⊔ |b|) ^ 0

Tactic:
simp [geomSum]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[simp] lemma inv_op_smul_set_distrib₀ (a : α) (s : Set α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹

Proof state:
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
α : Type u_2
inst✝ : GroupWithZero α
s : Set α
⊢ (op 0 • s)⁻¹ = 0⁻¹ • s⁻¹

case inr
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Proof state:
case inr.h
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (op a • s)⁻¹ ↔ x✝ ∈ a⁻¹ • s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀, *]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝ : GroupWithZero α
s : Set α
⊢ (op 0 • s)⁻¹ = 0⁻¹ • s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext

Result:
case inr.h
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (op a • s)⁻¹ ↔ x✝ ∈ a⁻¹ • s⁻¹