harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_eq_top_iff_of_nonempty {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    s.direction = ⊤ ↔ s = ⊤

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤.direction
⊢ s = ⊤

Tactic:
refine ext_of_direction_eq hd ?_

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤.direction
⊢ (↑s ∩ ↑⊤).Nonempty

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤
⊢ s = ⊤

Tactic:
rw [← direction_top k V P] at hd

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤.direction
⊢ s = ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s.direction = ⊤ ↔ s = ⊤

Tactic:
constructor

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s.direction = ⊤ → s = ⊤

case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s = ⊤ → s.direction = ⊤

Proof state:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : (↑⊤).Nonempty
⊢ ⊤.direction = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s.direction = ⊤ → s = ⊤

Tactic:
intro hd

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤
⊢ s = ⊤

Proof state:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s = ⊤ → s.direction = ⊤

Tactic:
rintro rfl

Result:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : (↑⊤).Nonempty
⊢ ⊤.direction = ⊤

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤.direction
⊢ (↑s ∩ ↑⊤).Nonempty

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem loop_eq {v : V} (p : G.Path v v) : p = Path.nil

Proof state:
case mk.cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
h : (Walk.cons h✝ p✝).IsPath
⊢ ⟨Walk.cons h✝ p✝, h⟩ = Path.nil

Tactic:
simp at h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Path v v
⊢ p = Path.nil

Tactic:
obtain ⟨_ | _, h⟩ := p

Result:
case mk.nil
V : Type u
G : SimpleGraph V
v : V
h : Walk.nil.IsPath
⊢ ⟨Walk.nil, h⟩ = Path.nil

case mk.cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
h : (Walk.cons h✝ p✝).IsPath
⊢ ⟨Walk.cons h✝ p✝, h⟩ = Path.nil

Proof state:
case mk.nil
V : Type u
G : SimpleGraph V
v : V
h : Walk.nil.IsPath
⊢ ⟨Walk.nil, h⟩ = Path.nil

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem exists_homeomorph_image_interior_closure_frontier_eq_unitBall {s : Set E}
    (hc : Convex ℝ s) (hne : (interior s).Nonempty) (hb : IsBounded s) :
    ∃ h : E ≃ₜ E, h '' interior s = ball 0 1 ∧ h '' closure s = closedBall 0 1 ∧
      h '' frontier s = sphere 0 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ ∃ h, ⇑h '' interior s = ball 0 1 ∧ ⇑h '' closure s = closedBall 0 1 ∧ ⇑h '' frontier s = sphere 0 1

Tactic:
simpa [isOpen_ball.interior_eq, closure_ball, frontier_ball]
  using exists_homeomorph_image_eq hc hne (NormedSpace.isVonNBounded_of_isBounded _ hb)
  (convex_ball 0 1) (by simp [isOpen_ball.interior_eq]) (NormedSpace.isVonNBounded_ball _ _ _)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ (interior (ball 0 1)).Nonempty

Tactic:
simp [isOpen_ball.interior_eq]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Kernels.lean
theorem cokernel_π_ext {M N : ModuleCat.{u} R} (f : M ⟶ N) {x y : N} (m : M) (w : x = y + f m) :
    cokernel.π f x = cokernel.π f y

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
y : ↑N
m : ↑M
⊢ (ConcreteCategory.hom (cokernel.π f)) (y + (ConcreteCategory.hom f) m) = (ConcreteCategory.hom (cokernel.π f)) y

Tactic:
simpa only [map_add, add_right_eq_self] using cokernel.condition_apply f m

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x y : ↑N
m : ↑M
w : x = y + (ConcreteCategory.hom f) m
⊢ (ConcreteCategory.hom (cokernel.π f)) x = (ConcreteCategory.hom (cokernel.π f)) y

Tactic:
subst w

Result:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
y : ↑N
m : ↑M
⊢ (ConcreteCategory.hom (cokernel.π f)) (y + (ConcreteCategory.hom f) m) = (ConcreteCategory.hom (cokernel.π f)) y
-- Mathlib/Order/Minimal.lean
theorem minimal_iff_minimal_of_imp_of_forall (hPQ : ∀ ⦃x⦄, Q x → P x)
    (h : ∀ ⦃x⦄, P x → ∃ y, y ≤ x ∧ Q y) : Minimal P x ↔ Minimal Q x

Proof state:
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
  fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩

Result:
case refine_1
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal P x
⊢ Q x

case refine_2
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y

Proof state:
case refine_1.intro.intro
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy : Q y
⊢ Q x

Tactic:
rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y

Tactic:
obtain ⟨z, hzy, hz⟩ := h hy

Result:
case refine_2.intro.intro
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
z : α
hzy : z ≤ y
hz : Q z
⊢ x ≤ y

Proof state:
case refine_2.intro.intro
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
z : α
hzy : z ≤ y
hz : Q z
⊢ x ≤ y

Tactic:
exact (h'.le_of_le hz (hzy.trans hyx)).trans hzy

Result:
no goals

Proof state:
case refine_1
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal P x
⊢ Q x

Tactic:
obtain ⟨y, hyx, hy⟩ := h h'.prop

Result:
case refine_1.intro.intro
α : Type u_1
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy : Q y
⊢ Q x
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

Proof state:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x < normalizedFactors y → DvdNotUnit x y

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y

Proof state:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y → normalizedFactors x < normalizedFactors y

Tactic:
rintro ⟨_, c, hc, rfl⟩

Result:
case mp.intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx left✝ : x ≠ 0
c : α
hc : ¬IsUnit c
hy : x * c ≠ 0
⊢ normalizedFactors x < normalizedFactors (x * c)

Proof state:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y

Tactic:
exact
  dvdNotUnit_of_dvd_of_not_dvd
    ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
    (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_le)

Result:
no goals

Proof state:
case mp.intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx left✝ : x ≠ 0
c : α
hc : ¬IsUnit c
hy : x * c ≠ 0
⊢ normalizedFactors x < normalizedFactors (x * c)

Tactic:
simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff,
  lt_add_iff_pos_right, normalizedFactors_pos, hc]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y → normalizedFactors x < normalizedFactors y

case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x < normalizedFactors y → DvdNotUnit x y
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_deriv_right_le_segment {f' : ℝ → E} {C : ℝ}
    (hf : ContinuousOn f (Icc a b)) (hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x)
    (bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C) : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
have hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x := by
  intro x hx
  simp [g, hf' x hx]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
let B x := C * (x - a)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_le_max_lift :
    #(FreeAlgebra R X) ≤ Cardinal.lift.{v} #R ⊔ Cardinal.lift.{u} #X ⊔ ℵ₀

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

Tactic:
exact (cardinalMk_eq_one R X).trans_le (le_max_of_le_right one_le_aleph0)

Result:
no goals

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

Tactic:
cases subsingleton_or_nontrivial R

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

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

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

Tactic:
exact (cardinalMk_eq_max_lift R X).le

Result:
no goals

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

Tactic:
cases isEmpty_or_nonempty X

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

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

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

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

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_add_one {n : ℕ} : Odd (n + 1) ↔ ¬ Odd n

Proof state:
n : ℕ
⊢ Odd (n + 1) ↔ ¬Odd n

Tactic:
rw [← not_even_iff_odd, Nat.even_add_one, not_even_iff_odd]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem norm_sup_sub_sup_le_add_norm (a b c d : α) : ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖

Proof state:
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|

Tactic:
exact abs_sup_sub_sup_le_abs _ _ _

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|

Tactic:
exact abs_sup_sub_sup_le_abs _ _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|

Tactic:
rw [sub_add_sub_cancel]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖

Tactic:
refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||

Proof state:
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|

Tactic:
rw [sup_comm c, sup_comm c]

Result:
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|

Tactic:
apply add_le_add

Result:
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|

case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||

Tactic:
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp]
lemma snd_add {μ ν : Measure (α × β)} : (μ + ν).snd = μ.snd + ν.snd

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure (α × β)
⊢ (μ + ν).snd = μ.snd + ν.snd

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ (μ + ν).snd s = (μ.snd + ν.snd) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ (μ + ν).snd s = (μ.snd + ν.snd) s

Tactic:
simp_rw [coe_add, Pi.add_apply, snd_apply hs, coe_add, Pi.add_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem sSup_le {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, g ≤ f) :
    sSup s ≤ f

Proof state:
case f.refine_2.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
b✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => Subtype.casesOn b fun g m => underlying.map (homOfLE ⋯)) ≫ f.arrow =
    Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫ smallCoproductDesc s

Tactic:
dsimp [smallCoproductDesc]

Result:
case f.refine_2.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
b✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => underlying.map (homOfLE ⋯)) ≫ f.arrow =
    Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      Sigma.desc fun j => ((equivShrink (Subobject A)).symm ↑j).arrow
-- Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
lemma iff_universallyClosed_and_isAffineHom {X Y : Scheme.{u}} {f : X ⟶ Y} :
    IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Proof state:
case intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Tactic:
wlog hX : ∃ S, X = Spec S

Result:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hX : ∃ S, X = Spec S
⊢ IsIntegralHom f

Proof state:
case intro.intro.h
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst✝¹ : Algebra ↑R ↑S := φ.hom'.toAlgebra
algInst✝ : Algebra (Polynomial ↑R) (Polynomial ↑S) := (Polynomial.mapRingHom φ.hom').toAlgebra
⊢ IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Tactic:
haveI : IsScalarTower R (Polynomial R) (Polynomial S) :=
  .of_algebraMap_eq' (Polynomial.mapRingHom_comp_C _).symm

Result:
case intro.intro.h
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst✝¹ : Algebra ↑R ↑S := φ.hom'.toAlgebra
algInst✝ : Algebra (Polynomial ↑R) (Polynomial ↑S) := (Polynomial.mapRingHom φ.hom').toAlgebra
this : IsScalarTower (↑R) (Polynomial ↑R) (Polynomial ↑S)
⊢ IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Proof state:
case intro.intro
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
apply PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom

Result:
case intro.intro.h
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Proof state:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)

Tactic:
exact this _ inferInstance inferInstance ⟨_, rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem bot_factors_iff_zero {A B : C} (f : A ⟶ B) : (⊥ : Subobject B).Factors f ↔ f = 0 :=
  ⟨by
    rintro ⟨h, rfl⟩
    simp only [MonoOver.bot_arrow_eq_zero, Functor.id_obj, Functor.const_obj_obj,
      MonoOver.bot_left, comp_zero],
   by
    rintro rfl
    exact ⟨0, by simp⟩⟩

Proof state:
case intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
h : A ⟶ ⊥.obj.left
⊢ h ≫ ⊥.arrow = 0

Tactic:
simp only [MonoOver.bot_arrow_eq_zero, Functor.id_obj, Functor.const_obj_obj,
  MonoOver.bot_left, comp_zero]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ 0 ≫ ⊥.arrow = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ ⊥.Factors 0

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
f : A ⟶ B
⊢ ⊥.Factors f → f = 0

Tactic:
rintro ⟨h, rfl⟩

Result:
case intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
h : A ⟶ ⊥.obj.left
⊢ h ≫ ⊥.arrow = 0

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
f : A ⟶ B
⊢ f = 0 → ⊥.Factors f

Tactic:
rintro rfl

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ ⊥.Factors 0