harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean
theorem of_iso (hY : IsZero Y) (e : X ≅ Y) : IsZero X

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default

Tactic:
apply hY.eq_of_src

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
⊢ IsZero X

Tactic:
refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
  fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default

Tactic:
rw [← cancel_epi e.inv]

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default

Tactic:
rw [← cancel_mono e.hom]

Result:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom

Tactic:
apply hY.eq_of_tgt

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem disjoint_span_singleton : Disjoint s (K ∙ x) ↔ x ∈ s → x = 0

Proof state:
case neg
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0

Tactic:
rw [s.smul_mem_iff hc] at hy

Result:
case neg
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0

Proof state:
case pos
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : c = 0
⊢ c • x = 0

Tactic:
rw [hc, zero_smul]

Result:
no goals

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
⊢ (x ∈ s → x = 0) → ∀ x_1 ∈ s, x_1 ∈ span K {x} → x_1 = 0

Tactic:
intro H y hy hyx

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
y : V
hy : y ∈ s
hyx : y ∈ span K {x}
⊢ y = 0

Proof state:
case neg
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0

Tactic:
rw [H hy, smul_zero]

Result:
no goals

Proof state:
case intro
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
⊢ c • x = 0

Tactic:
by_cases hc : c = 0

Result:
case pos
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : c = 0
⊢ c • x = 0

case neg
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
hc : ¬c = 0
⊢ c • x = 0

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
⊢ Disjoint s (span K {x}) ↔ x ∈ s → x = 0

Tactic:
refine disjoint_def.trans ⟨fun H hx => H x hx <| subset_span <| mem_singleton x, ?_⟩

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
⊢ (x ∈ s → x = 0) → ∀ x_1 ∈ s, x_1 ∈ span K {x} → x_1 = 0

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
y : V
hy : y ∈ s
hyx : y ∈ span K {x}
⊢ y = 0

Tactic:
obtain ⟨c, rfl⟩ := mem_span_singleton.1 hyx

Result:
case intro
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
H : x ∈ s → x = 0
c : K
hy : c • x ∈ s
hyx : c • x ∈ span K {x}
⊢ c • x = 0
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem convexOn_Gamma : ConvexOn ℝ (Ioi 0) Gamma

Proof state:
x : ℝ
hx : x ∈ Ioi 0
m : ℕ
⊢ x ≠ -↑m

Tactic:
exact (neg_lt_iff_pos_add.mpr (add_pos_of_pos_of_nonneg (mem_Ioi.mp hx) (Nat.cast_nonneg m))).ne'

Result:
no goals

Proof state:
⊢ Convex ℝ (log ∘ Gamma '' Ioi 0)

Tactic:
rw [convex_iff_isPreconnected]

Result:
⊢ IsPreconnected (log ∘ Gamma '' Ioi 0)

Proof state:
⊢ ConvexOn ℝ (Ioi 0) Gamma

Tactic:
refine
  ((convexOn_exp.subset (subset_univ _) ?_).comp convexOn_log_Gamma
        (exp_monotone.monotoneOn _)).congr
    fun x hx => exp_log (Gamma_pos_of_pos hx)

Result:
⊢ Convex ℝ (log ∘ Gamma '' Ioi 0)

Proof state:
x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (log ∘ Gamma) x

Tactic:
refine (differentiableAt_Gamma fun m => ?_).continuousAt.log (Gamma_pos_of_pos hx).ne'

Result:
x : ℝ
hx : x ∈ Ioi 0
m : ℕ
⊢ x ≠ -↑m

Proof state:
⊢ IsPreconnected (log ∘ Gamma '' Ioi 0)

Tactic:
refine isPreconnected_Ioi.image _ fun x hx => ContinuousAt.continuousWithinAt ?_

Result:
x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (log ∘ Gamma) x
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem image_eq {Δ Δ' Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ Δ'} [Epi e] {i : Δ' ⟶ Δ''}
    [Mono i] (fac : e ≫ i = φ) : image φ = Δ'

Proof state:
case a
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ (image φ).len = Δ'.len

Tactic:
exact
  le_antisymm (len_le_of_epi (inferInstance : Epi e.hom))
    (len_le_of_mono (inferInstance : Mono e.hom))

Result:
no goals

Proof state:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image φ = Δ'

Tactic:
let e := image.isoStrongEpiMono e i fac

Result:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'

Proof state:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image φ = Δ'

Tactic:
haveI := strongEpi_of_epi e

Result:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image φ = Δ'

Proof state:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'

Tactic:
ext

Result:
case a
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ (image φ).len = Δ'.len
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem le_iff (S T : Subgroupoid C) : S ≤ T ↔ ∀ {c d}, S.arrows c d ⊆ T.arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ (∀ (a : C) (b : (d : C) × (a ⟶ d)), ⟨a, b⟩ ∈ S → ⟨a, b⟩ ∈ T) ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
exact forall_congr' fun c => Sigma.forall

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
rw [SetLike.le_def, Sigma.forall]

Result:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ (∀ (a : C) (b : (d : C) × (a ⟶ d)), ⟨a, b⟩ ∈ S → ⟨a, b⟩ ∈ T) ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
-- Mathlib/Analysis/Convex/Function.lean
theorem convexOn_iff_forall_pos {s : Set E} {f : E → β} :
    ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b →
      a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
obtain rfl | hb' := hb.eq_or_lt

Result:
case inr.inl
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ f (a • x + 0 • y) ≤ a • f x + 0 • f y

case inr.inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
⊢ f (a • x + b • y) ≤ a • f x + b • f y
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_one : valuation (1 : ℚ_[p]) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 1 = 0

Tactic:
rw [← Nat.cast_one, valuation_natCast, padicValNat.one, cast_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem isSome_unattach {p : α → Prop} {o : Option { x // p x }} :
    o.unattach.isSome = o.isSome

Proof state:
α : Type u_1
p : α → Prop
o : Option { x // p x }
⊢ o.unattach.isSome = o.isSome

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
lemma measure_support_lt_top (f : α →ₛ β) (hf : ∀ y, y ≠ 0 → μ (f ⁻¹' {y}) < ∞) :
    μ (support f) < ∞

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (support ⇑f) < ⊤

Tactic:
classical
rw [support_eq]
refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
rw [Finset.mem_filter] at hy
exact hf y hy.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ filter (fun y => y ≠ 0) f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
rw [Finset.mem_filter] at hy

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ f.range ∧ y ≠ 0
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (support ⇑f) < ⊤

Tactic:
rw [support_eq]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y}) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y}) < ⊤

Tactic:
refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ filter (fun y => y ≠ 0) f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ f.range ∧ y ≠ 0
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
exact hf y hy.2

Result:
no goals
-- Mathlib/Algebra/Small/Group.lean
@[to_additive (attr := simp)]
lemma equivShrink_symm_div [Div α] [Small α] (x y : Shrink α) :
    (equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y

Proof state:
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y

Tactic:
rw [Equiv.div_def]

Result:
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x / (equivShrink α).symm y)) =
    (equivShrink α).symm x / (equivShrink α).symm y

Proof state:
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x / (equivShrink α).symm y)) =
    (equivShrink α).symm x / (equivShrink α).symm y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_left_Icc (a b c : α) :
    (Icc a b).map (addLeftEmbedding c) = Icc (c + a) (c + b)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)

Tactic:
exact Set.image_const_add_Icc _ _ _

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem chainClosure_succ_total (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂)
    (h : c₁ ⊆ c₂) : c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂

Proof state:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ⋃₀ s✝ = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝

Tactic:
apply Or.imp_left h.antisymm'

Result:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ⋃₀ s✝ ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_smul' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞) :
    μ.withDensity (r • f) = r • μ.withDensity f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s

Tactic:
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
  smul_eq_mul, ← lintegral_const_mul' r f hr]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
refine Measure.ext fun s hs => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s
-- Mathlib/Algebra/GradedMonoid.lean
theorem pow_mem_graded (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i)

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ 0 ∈ A (0 • i)

Tactic:
rw [pow_zero, zero_nsmul]

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)

Tactic:
rw [pow_succ', succ_nsmul']

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)

Tactic:
exact mul_mem_graded h (pow_mem_graded n h)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)

Tactic:
match n with
| 0 =>
  rw [pow_zero, zero_nsmul]
  exact one_mem_graded _
| n+1 =>
  rw [pow_succ', succ_nsmul']
  exact mul_mem_graded h (pow_mem_graded n h)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0

Tactic:
exact one_mem_graded _

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
lemma Icc_inr_inr :
    Icc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Icc b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Icc b₁ b₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem udiv_self {x : BitVec w} :
    x / x = if x == 0#w then 0#w else 1#w

Proof state:
w : Nat
x : BitVec w
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

Tactic:
by_cases h : x = 0#w

Result:
case pos
w : Nat
x : BitVec w
h : x = 0#w
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

case neg
w : Nat
x : BitVec w
h : ¬x = 0#w
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

Proof state:
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ 0 < x.toNat

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
h : x = 0#w
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

Tactic:
simp only [udiv_eq, beq_iff_eq, toNat_eq, toNat_ofNat, Nat.zero_mod, h,
  ↓reduceIte, toNat_udiv]

Result:
case neg
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ x.toNat / x.toNat = 1 % 2 ^ w

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ x.toNat / x.toNat = 1 % 2 ^ w

Tactic:
rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x = 0#w
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

Tactic:
simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h

Result:
case neg
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ x / x = if (x == 0#w) = true then 0#w else 1#w

Proof state:
w : Nat
x : BitVec w
h : ¬x.toNat = 0
⊢ 1 < 2 ^ w

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finset/Defs.lean
@[simp] lemma forall_mem_not_eq {s : Finset α} {a : α} : (∀ b ∈ s, ¬ a = b) ↔ a ∉ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ s, ¬a = b) ↔ a ∉ s

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem coeff_one_reverse (f : R[X]) : coeff (reverse f) 1 = nextCoeff f

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.coeff 1 = f.nextCoeff

Tactic:
rw [coeff_reverse, nextCoeff]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree

Tactic:
exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree) 1) = 0

Tactic:
have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
this : f.coeff 1 = 0
⊢ f.coeff ((revAt f.natDegree) 1) = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
this : f.coeff 1 = 0
⊢ f.coeff ((revAt f.natDegree) 1) = 0

Tactic:
simp [*, revAt]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)

Tactic:
split_ifs with hf

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree) 1) = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree) 1) = f.coeff (f.natDegree - 1)

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.natDegree < 1

Tactic:
simp only [hf, zero_lt_one]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree) 1) = f.coeff (f.natDegree - 1)

Tactic:
rw [revAt_le]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree
-- Mathlib/Control/Traversable/Lemmas.lean
theorem map_traverse' (g : α → G β) (h : β → γ) :
    traverse (map h ∘ g) = (map (map h) ∘ traverse g : t α → G (t γ))

Proof state:
case h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
x✝ : t α
⊢ traverse (map h ∘ g) x✝ = (map (map h) ∘ traverse g) x✝

Tactic:
rw [comp_apply, map_traverse]

Result:
no goals

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
⊢ traverse (map h ∘ g) = map (map h) ∘ traverse g

Tactic:
ext

Result:
case h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
x✝ : t α
⊢ traverse (map h ∘ g) x✝ = (map (map h) ∘ traverse g) x✝