harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem right_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : y ≠ 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y ≠ 0
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : o.oangle x 0 ≠ 0
⊢ False

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : o.oangle x 0 ≠ 0
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg {x y : ℝ*} :
    InfinitePos x → ¬Infinitesimal y → y < 0 → InfiniteNeg (x * y)

Proof state:
x y : ℝ*
⊢ x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]

Result:
x y : ℝ*
⊢ x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos

Proof state:
x y : ℝ*
⊢ x.InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (x * -y).InfinitePos

Tactic:
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem units_inv_apply_apply (f : CircleDeg1Liftˣ) (x : ℝ) :
    (f⁻¹ : CircleDeg1Liftˣ) (f x) = x

Proof state:
f : CircleDeg1Liftˣ
x : ℝ
⊢ ↑f⁻¹ (↑f x) = x

Tactic:
simp only [← mul_apply, f.inv_mul, coe_one, id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as

Proof state:
α : Type u_1
x : α
as : Array α
⊢ x ∈ as.reverse ↔ x ∈ as

Tactic:
cases as

Result:
case mk
α : Type u_1
x : α
toList✝ : List α
⊢ x ∈ { toList := toList✝ }.reverse ↔ x ∈ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
x : α
toList✝ : List α
⊢ x ∈ { toList := toList✝ }.reverse ↔ x ∈ { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem exists_reduced_factors :
    ∀ a ≠ (0 : R), ∀ b,
      ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Proof state:
case pos.intro
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b

Tactic:
obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b

Result:
case pos.intro.intro.intro.intro.intro.intro
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b

Proof state:
case pos.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a

Tactic:
rw [mul_assoc, ha']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_dropLast {xs : List α} :
    xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]?

Proof state:
case isFalse.hc
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs.dropLast.length - 1 < xs.length - 1

Tactic:
simp only [Nat.not_le] at h

Result:
case isFalse.hc
α : Type u_1
xs : List α
h : 1 < xs.length
⊢ xs.dropLast.length - 1 < xs.length - 1

Proof state:
α : Type u_1
xs : List α
h : xs.length ≤ 1
head✝ : α
x✝ : [head✝].length ≤ 1
⊢ [head✝].dropLast.getLast? = none

Tactic:
simp

Result:
no goals

Proof state:
case isTrue
α : Type u_1
xs : List α
h : xs.length ≤ 1
⊢ xs.dropLast.getLast? = none

Tactic:
match xs, h with
| [], _
| [_], _ => simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]?

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
xs : List α
h : xs.length ≤ 1
⊢ xs.dropLast.getLast? = none

case isFalse
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs.dropLast.getLast? = xs[xs.length - 2]?

Proof state:
case isFalse
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs.dropLast.getLast? = xs[xs.length - 2]?

Tactic:
rw [getLast?_eq_getElem?, getElem?_dropLast, if_pos]

Result:
case isFalse
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs[xs.dropLast.length - 1]? = xs[xs.length - 2]?

case isFalse.hc
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs.dropLast.length - 1 < xs.length - 1

Proof state:
case isFalse
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs[xs.dropLast.length - 1]? = xs[xs.length - 2]?

Tactic:
congr 1

Result:
case isFalse.e_a
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs.dropLast.length - 1 = xs.length - 2

Proof state:
α : Type u_1
xs : List α
h : 1 < xs.length
head✝¹ head✝ : α
tail✝ : List α
x✝ : 1 < (head✝¹ :: head✝ :: tail✝).length
⊢ (head✝¹ :: head✝ :: tail✝).dropLast.length - 1 < (head✝¹ :: head✝ :: tail✝).length - 1

Tactic:
simp

Result:
no goals

Proof state:
case isFalse.hc
α : Type u_1
xs : List α
h : 1 < xs.length
⊢ xs.dropLast.length - 1 < xs.length - 1

Tactic:
match xs, h with
| (_ :: _ :: _), _ => simp

Result:
no goals

Proof state:
case isFalse.e_a
α : Type u_1
xs : List α
h : ¬xs.length ≤ 1
⊢ xs.dropLast.length - 1 = xs.length - 2

Tactic:
simp [← Nat.sub_add_eq]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean
@[simp]
lemma sectionMap_freeMap_freeSection (i : I) :
    sectionsMap (freeMap (R := R) f) (freeSection i) = freeSection (f i)

Proof state:
C : Type u'
inst✝³ : Category.{v', u'} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝² : HasWeakSheafify J✝ AddCommGrp
inst✝¹ : J✝.WEqualsLocallyBijective AddCommGrp
inst✝ : J✝.HasSheafCompose (forget₂ RingCat AddCommGrp)
I J : Type u
f : I → J
i : I
⊢ sectionsMap (freeMap f) (freeSection i) = freeSection (f i)

Tactic:
simp [← freeHomEquiv_comp_apply]

Result:
no goals
-- Mathlib/Probability/Distributions/Pareto.lean
lemma paretoPDF_of_le (hx : t ≤ x) :
    paretoPDF t r x = ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))

Proof state:
t r x : ℝ
hx : t ≤ x
⊢ paretoPDF t r x = ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))

Tactic:
simp only [paretoPDF_eq, if_pos hx]

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_of_nonpos {n : ℤ} (hn : n ≤ 0) :
    selfZPow x B n = mk' _ (1 : R) (Submonoid.pow x n.natAbs)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
by_cases hn0 : n = 0

Result:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Proof state:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
simp [hn0, selfZPow_zero, Submonoid.pow_apply]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
simp [selfZPow_of_neg _ _ (lt_of_le_of_ne hn hn0)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem ne_zero (hp : p.IsUnitTrinomial) : p ≠ 0

Proof state:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
hp : IsUnitTrinomial 0
⊢ False

Proof state:
hp : IsUnitTrinomial 0
⊢ False

Tactic:
simpa using hp.card_support_eq_three

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem coe_closure_eq (s : Set R) :
    (closure s : Set R) = AddSubmonoid.closure (Submonoid.closure s : Set R)

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
⊢ ↑(closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))

Tactic:
simp [← Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem head_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) (h : xs.pmap f H ≠ []) :
    (xs.pmap f H).head h = f (xs.head (by simpa using h)) (H _ (head_mem _))

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : pmap f xs H ≠ []
⊢ (pmap f xs H).head h = f (xs.head ⋯) ⋯

Tactic:
induction xs with
| nil => simp at h
| cons x xs ih => simp [head_pmap, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ [] → P a
h : pmap f [] H ≠ []
⊢ (pmap f [] H).head h = f ([].head ⋯) ⋯

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type ?u.45771
β : Type ?u.45807
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : pmap f xs H ≠ []
⊢ xs ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
x : α
xs : List α
ih : ∀ (H : ∀ (a : α), a ∈ xs → P a) (h : pmap f xs H ≠ []), (pmap f xs H).head h = f (xs.head ⋯) ⋯
H : ∀ (a : α), a ∈ x :: xs → P a
h : pmap f (x :: xs) H ≠ []
⊢ (pmap f (x :: xs) H).head h = f ((x :: xs).head ⋯) ⋯

Tactic:
simp [head_pmap, ih]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_range_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    range (map f g) = Submodule.span R { t | ∃ m n, f m ⊗ₜ g n = t }

Proof state:
case e_s.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}

Tactic:
constructor

Result:
case e_s.h.mp
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t} → t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t}

case e_s.h.mpr
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ t ∈ {t | ∃ m n, f m ⊗ₜ[R] g n = t} → t ∈ ⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}
-- Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
theorem IsCountablySpanning.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
    IsCountablySpanning (pi univ '' pi univ C)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
cases nonempty_encodable (ι → ℕ)

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => (decode n).iget
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => (decode n).iget
⊢ ⋃ n, (fun n => univ.pi fun i => s i (e n i)) n = univ

Tactic:
simp_rw
  [e, (surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
  iUnion_univ_pi s, h2s, pi_univ]

Result:
no goals

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => (decode n).iget
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
refine ⟨fun n => Set.pi univ fun i => s i (e n i), fun n =>
  mem_image_of_mem _ fun i _ => h1s i _, ?_⟩

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => (decode n).iget
⊢ ⋃ n, (fun n => univ.pi fun i => s i (e n i)) n = univ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
choose s h1s h2s using hC

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
⊢ IsCountablySpanning (univ.pi '' univ.pi C)
-- Mathlib/Order/Defs/LinearOrder.lean
lemma max_assoc (a b c : α) : max (max a b) c = max a (max b c)

Proof state:
case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ max (max a b) c

Tactic:
apply le_trans (le_max_left a b) (le_max_left ..)

Result:
no goals

Proof state:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ b ≤ d

Tactic:
apply le_trans (le_max_left _ _) h₂

Result:
no goals

Proof state:
case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ max b c ≤ max (max a b) c

Tactic:
apply max_le

Result:
case h₂.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ≤ max (max a b) c

case h₂.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ c ≤ max (max a b) c

Proof state:
case h₂.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ≤ max (max a b) c

Tactic:
apply le_trans (le_max_right a b) (le_max_left ..)

Result:
no goals

Proof state:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ max a b ≤ d

Tactic:
apply max_le h₁

Result:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ b ≤ d

Proof state:
case h₂.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ c ≤ max (max a b) c

Tactic:
apply le_max_right

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ max (max a b) c = max a (max b c)

Tactic:
apply eq_max

Result:
case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ max (max a b) c

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ max b c ≤ max (max a b) c

case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ d

Proof state:
case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ max (max a b) c ≤ d

Tactic:
apply max_le

Result:
case h₃.h₁
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ max a b ≤ d

case h₃.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ c ≤ d

Proof state:
case h₃.h₂
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ c ≤ d

Tactic:
apply le_trans (le_max_right _ _) h₂

Result:
no goals

Proof state:
case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ d

Tactic:
intro d h₁ h₂

Result:
case h₃
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ max (max a b) c ≤ d
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_disj_sum (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) :
    ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α ⊕ γ → β
⊢ ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α ⊕ γ → β
⊢ (∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ t, f (Embedding.inr x) = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α ⊕ γ → β
⊢ (∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ t, f (Embedding.inr x) = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma in₁₀_iff' :
    (graph t).Adj (in₁ b) (in₀ a) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.2.1 = b ∧ x.1 = a where
  mp

Proof state:
case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a

Tactic:
exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
⊢ (graph t).Adj (in₁ b) (in₀ a) → ∃ x ∈ t, x.2.1 = b ∧ x.1 = a

Tactic:
rintro ⟨⟩

Result:
case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a

Proof state:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, (a, b, c).2.1, ?intro.mk.mk.intro.intro.c) ∈ t

case intro.mk.mk.intro.intro.c
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ γ

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
⊢ (∃ x ∈ t, x.2.1 = b ∧ x.1 = a) → (graph t).Adj (in₁ b) (in₀ a)

Tactic:
rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩

Result:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₀ (a, b, c).1)

Proof state:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₀ (a, b, c).1)

Tactic:
constructor

Result:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, (a, b, c).2.1, ?intro.mk.mk.intro.intro.c) ∈ t

case intro.mk.mk.intro.intro.c
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ γ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ (a, b, c✝).2.1 = b ∧ (a, b, c✝).1 = a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Exposed.lean
theorem isClosed [OrderClosedTopology 𝕜] {A B : Set E} (hAB : IsExposed 𝕜 A B)
    (hA : IsClosed A) : IsClosed B

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
⊢ IsClosed B

Tactic:
obtain rfl | hB := B.eq_empty_or_nonempty

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed ∅

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : B.Nonempty
⊢ IsClosed B

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed ∅

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : E →L[𝕜] 𝕜
a : 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ a ≤ l x}
hB : {x | x ∈ A ∧ a ≤ l x}.Nonempty
⊢ IsClosed {x | x ∈ A ∧ a ≤ l x}

Tactic:
exact hA.isClosed_le continuousOn_const l.continuous.continuousOn

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : B.Nonempty
⊢ IsClosed B

Tactic:
obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfSpace' hB

Result:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : E →L[𝕜] 𝕜
a : 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ a ≤ l x}
hB : {x | x ∈ A ∧ a ≤ l x}.Nonempty
⊢ IsClosed {x | x ∈ A ∧ a ≤ l x}
-- Mathlib/Order/LiminfLimsup.lean
theorem IsBoundedUnder.mono_le [Preorder β] {l : Filter α} {u v : α → β}
    (hu : IsBoundedUnder (· ≤ ·) l u) (hv : v ≤ᶠ[l] u) : IsBoundedUnder (· ≤ ·) l v

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l v

Tactic:
apply hu.imp

Result:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β), (∀ᶠ (x : β) in map u l, (fun x1 x2 => x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun x1 x2 => x1 ≤ x2) x a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β), (∀ᶠ (x : β) in map u l, (fun x1 x2 => x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun x1 x2 => x1 ≤ x2) x a

Tactic:
exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

Result:
no goals