harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Cardinal.lean
theorem cardinalMk_le_max_lift {σ : Type u} {R : Type v} [CommSemiring R] : #(MvPolynomial σ R) ≤
    max (max (Cardinal.lift.{u} #R) <| Cardinal.lift.{v} #σ) ℵ₀

Proof state:
case inr.inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
exact cardinalMk_eq_max_lift.le

Result:
no goals

Proof state:
case inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
cases isEmpty_or_nonempty σ

Result:
case inr.inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

case inr.inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Proof state:
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

case inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Proof state:
case inr.inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
exact cardinalMk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)

Result:
no goals

Proof state:
case inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ #(MvPolynomial σ R) ≤ lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem Nonempty.of_disjSups_right : (s ○ t).Nonempty → t.Nonempty

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (s ○ t).Nonempty → t.Nonempty

Tactic:
simp_rw [Finset.Nonempty, mem_disjSups]

Result:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ t

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ t

Tactic:
exact fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_support {u v : V} (p : G.Walk u v) : p.support.length = p.length + 1

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support.length = p.length + 1

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
private lemma farFromTriangleFree_of_disjoint_triangles_aux {tris : Finset (Finset α)}
    (htris : tris ⊆ G.cliqueFinset 3)
    (pd : (tris : Set (Finset α)).Pairwise fun x y ↦ (x ∩ y : Set α).Subsingleton) (hHG : H ≤ G)
    (hH : H.CliqueFree 3) : #tris ≤ #G.edgeFinset - #H.edgeFinset

Proof state:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
⊢ False

Tactic:
let f (t : {x // x ∈ tris}) : Sym2 α := s(fx t.2, fy t.2)

Result:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → t ∈ tris → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : { x // x ∈ tris } → Sym2 α := fun t => s(fx ⋯, fy ⋯)
⊢ False
-- Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
theorem auxEquiv_one : auxEquiv R 𝒜 ℬ 1 = 1

Proof state:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝¹ : GradedAlgebra 𝒜
inst✝ : GradedAlgebra ℬ
⊢ (auxEquiv R 𝒜 ℬ) 1 = 1

Tactic:
rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
  DirectSum.decompose_one, Algebra.TensorProduct.one_def]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma homologyπ_naturality (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] :
    S₁.homologyπ ≫ homologyMap φ = cyclesMap φ ≫ S₂.homologyπ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₁.homologyπ ≫ homologyMap φ = cyclesMap φ ≫ S₂.homologyπ

Tactic:
simp only [← cancel_mono S₂.leftHomologyIso.inv, assoc, ← leftHomologyIso_inv_naturality φ,
  homologyπ_comp_leftHomologyIso_inv]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₁.homologyπ ≫ S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = cyclesMap φ ≫ S₂.leftHomologyπ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₁.homologyπ ≫ S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = cyclesMap φ ≫ S₂.leftHomologyπ

Tactic:
simp only [homologyπ, assoc, Iso.hom_inv_id_assoc, leftHomologyπ_naturality]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α}
    {x₀ : X'} {k : κ} (hk : EquicontinuousAt (tX := t k) F x₀) :
    EquicontinuousAt (tX := ⨅ k, t k) F x₀

Proof state:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F univ x₀
⊢ EquicontinuousWithinAt F univ x₀

Tactic:
exact equicontinuousWithinAt_iInf_dom hk

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousAt F x₀
⊢ EquicontinuousAt F x₀

Tactic:
rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢

Result:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F univ x₀
⊢ EquicontinuousWithinAt F univ x₀
-- Mathlib/Data/Complex/Basic.lean
/-- A vertical segment `[b₁, b₂]` translated by `a` is the complex line segment. -/
lemma verticalSegment_eq (a b₁ b₂ : ℝ) :
    (fun (y : ℝ) ↦ a + y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]]

Proof state:
case h.mpr
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]] → x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]

Tactic:
intro hx

Result:
case h.mpr
a b₁ b₂ : ℝ
x : ℂ
hx : x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]

Proof state:
case h.mpr
a b₁ b₂ : ℝ
x : ℂ
hx : x.im ∈ [[b₁, b₂]] ∧ a = x.re
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]

Tactic:
obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx

Result:
case h.mpr.intro.refl
b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ x ∈ (fun y => ↑x.re + ↑y * I) '' [[b₁, b₂]]

Proof state:
case h.mpr.intro.refl
b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ x ∈ (fun y => ↑x.re + ↑y * I) '' [[b₁, b₂]]

Tactic:
refine ⟨x.im, x₁, by simp⟩

Result:
no goals

Proof state:
case h.mp
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] → x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
intro hx

Result:
case h.mp
a b₁ b₂ : ℝ
x : ℂ
hx : x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Proof state:
case h.mpr
a b₁ b₂ : ℝ
x : ℂ
hx : x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]

Tactic:
simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq,
  exists_eq_right_right, mem_preimage] at hx

Result:
case h.mpr
a b₁ b₂ : ℝ
x : ℂ
hx : x.im ∈ [[b₁, b₂]] ∧ a = x.re
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]

Proof state:
a b₁ b₂ : ℝ
⊢ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] = ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
ext x

Result:
case h
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Proof state:
b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ (fun y => ↑x.re + ↑y * I) x.im = x

Tactic:
simp

Result:
no goals

Proof state:
case h
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
constructor

Result:
case h.mp
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] → x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

case h.mpr
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]] → x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]

Proof state:
case h.mp.intro.intro
a b₁ b₂ : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[b₁, b₂]]
hx₁' : (fun y => ↑a + ↑y * I) x₁ = x
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
simp [← hx₁', mem_preimage, mem_prod, hx₁]

Result:
no goals

Proof state:
case h.mp
a b₁ b₂ : ℝ
x : ℂ
hx : x ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
obtain ⟨x₁, hx₁, hx₁'⟩ := hx

Result:
case h.mp.intro.intro
a b₁ b₂ : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[b₁, b₂]]
hx₁' : (fun y => ↑a + ↑y * I) x₁ = x
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Proof state:
a b₁ b₂ : ℝ
⊢ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]]

Tactic:
rw [← preimage_equivRealProd_prod]

Result:
a b₁ b₂ : ℝ
⊢ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]] = ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_monomial (s : σ →₀ ℕ) {c : R} (hc : c ≠ 0) :
    (monomial s c : MvPolynomial σ R).totalDegree = s.sum fun _ e => e

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ ((monomial s) c).totalDegree = s.sum fun x e => e

Tactic:
classical simp [totalDegree, support_monomial, if_neg hc]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ ((monomial s) c).totalDegree = s.sum fun x e => e

Tactic:
simp [totalDegree, support_monomial, if_neg hc]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem mem_lookupAll {a : α} {b : β a} :
    ∀ {l : List (Sigma β)}, b ∈ lookupAll a l ↔ Sigma.mk a b ∈ l
  | [] => by simp
  | ⟨a', b'⟩ :: l => by
    by_cases h : a = a'
    · subst h
      simp [*, mem_lookupAll]
    · simp [*, mem_lookupAll]

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
subst h

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
⊢ b ∈ lookupAll a (⟨a, b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
simp [*, mem_lookupAll]

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
⊢ b ∈ lookupAll a (⟨a, b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Tactic:
simp [*, mem_lookupAll]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ lookupAll a [] ↔ ⟨a, b⟩ ∈ []

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem isPreconnected_Icc_aux (x y : α) (s t : Set α) (hxy : x ≤ y) (hs : IsClosed s)
    (ht : IsClosed t) (hab : Icc a b ⊆ s ∪ t) (hx : x ∈ Icc a b ∩ s) (hy : y ∈ Icc a b ∩ t) :
    (Icc a b ∩ (s ∩ t)).Nonempty

Proof state:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[Ioc z y] z

Tactic:
exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this✝ : tᶜ ∩ Ioc z y ∈ 𝓝[>] z
this : Ioc z y ⊆ s ∪ t
⊢ tᶜ ∩ Ioc z y ⊆ s

Tactic:
exact fun w ⟨wt, wzy⟩ => (this wzy).elim id fun h => (wt h).elim

Result:
no goals

Proof state:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
⊢ s ∈ 𝓝[>] z

Tactic:
have zt : z ∈ tᶜ := fun zt => hst ⟨z, xyab <| Ico_subset_Icc_self hz, zs, zt⟩

Result:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed s
ht : IsClosed t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ s ∈ 𝓝[>] z
-- Mathlib/Data/Finsupp/Defs.lean
theorem embDomain_mapRange (f : α ↪ β) (g : M → N) (p : α →₀ M) (hg : g 0 = 0) :
    embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p)

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a' : α
⊢ (embDomain f (mapRange g hg p)) (f a') = (mapRange g hg (embDomain f p)) (f a')

Tactic:
rw [mapRange_apply, embDomain_apply, embDomain_apply, mapRange_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
⊢ embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p)

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
⊢ (embDomain f (mapRange g hg p)) a = (mapRange g hg (embDomain f p)) a

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f (mapRange g hg p)) a = (mapRange g hg (embDomain f p)) a

Tactic:
rw [mapRange_apply, embDomain_notin_range, embDomain_notin_range, ← hg] <;> assumption

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f (mapRange g hg p)) a = (mapRange g hg (embDomain f p)) a

Tactic:
rcases h with ⟨a', rfl⟩

Result:
case pos.intro
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a' : α
⊢ (embDomain f (mapRange g hg p)) (f a') = (mapRange g hg (embDomain f p)) (f a')

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
⊢ (embDomain f (mapRange g hg p)) a = (mapRange g hg (embDomain f p)) a

Tactic:
by_cases h : a ∈ Set.range f

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f (mapRange g hg p)) a = (mapRange g hg (embDomain f p)) a

case neg
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f (mapRange g hg p)) a = (mapRange g hg (embDomain f p)) a
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma distinguished_cocone_triangle {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    ∃ (Z : Cᵒᵖ) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧),
      Triangle.mk f g h ∈ distinguishedTriangles C

Proof state:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Triangle.mk f g.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op) ∈
    distinguishedTriangles C

Tactic:
simp only [mem_distinguishedTriangles_iff]

Result:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop
      ((triangleOpEquivalence C).inverse.obj
        (Triangle.mk f g.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op))) ∈
    Pretriangulated.distinguishedTriangles

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ ((Opposite.unop
            ((triangleOpEquivalence C).inverse.obj
              (Triangle.mk f g.op
                ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                  (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₃ ≫
        (shiftFunctor C 1).map
          (Iso.refl
              (Opposite.unop
                  ((triangleOpEquivalence C).inverse.obj
                    (Triangle.mk f g.op
                      ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                        (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₁).hom).op =
    ((Iso.refl
            (Opposite.unop
                ((triangleOpEquivalence C).inverse.obj
                  (Triangle.mk f g.op
                    ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                      (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₃).hom ≫
        (Triangle.mk g f.unop h).mor₃).op

Tactic:
simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_inf_sdiff : x \ y ⊓ y \ x = ⊥ :=
  Eq.symm <|
    calc
      ⊥ = x ⊓ y ⊓ x \ y

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

Tactic:
rw [inf_sup_left]

Result:
no goals

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

Tactic:
rw [inf_idem]

Result:
no goals

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

Tactic:
rw [inf_inf_sdiff]

Result:
no goals

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

Tactic:
rw [inf_of_le_right sdiff_le']

Result:
no goals

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

Tactic:
ac_rfl

Result:
no goals

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

Tactic:
rw [inf_sup_right, inf_comm x y]

Result:
no goals

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

Tactic:
rw [inf_inf_sdiff, bot_sup_eq]

Result:
no goals

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

Tactic:
rw [sup_inf_sdiff]

Result:
no goals

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

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_eval_one (n : ℕ) : (bernoulli n).eval 1 = bernoulli' n

Proof state:
n : ℕ
⊢ ∑ i ∈ range (n + 1), eval 1 ((monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i))) = bernoulli' n

Tactic:
simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self,
  (_root_.bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, eval_C, eval_monomial, one_mul]

Result:
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Proof state:
case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
simp [h, bernoulli_eq_bernoulli'_of_ne_one h]

Result:
no goals

Proof state:
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
by_cases h : n = 1

Result:
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Proof state:
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
norm_num [h]

Result:
no goals

Proof state:
n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n

Tactic:
simp only [bernoulli, eval_finset_sum]

Result:
n : ℕ
⊢ ∑ i ∈ range (n + 1), eval 1 ((monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i))) = bernoulli' n