harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι → Set α}
    (H : ∀ i ∈ t, IsPreconnected (s i))
    (K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) :
    IsPreconnected (⋃ n ∈ t, s n)

Proof state:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Proof state:
case tail.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ IsPreconnected (⋃ j ∈ insert k p, s j)

Tactic:
rw [biUnion_insert]

Result:
case tail.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ IsPreconnected (s k ∪ ⋃ x ∈ p, s x)
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_add {c' : E} :
    indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' =
    indicatorConstLp p hs hμs (c + c')

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c c' : E
⊢ MemLp.toLp ((s.indicator fun x => c) + s.indicator fun x => c') ⋯ =
    MemLp.toLp (fun a => s.indicator (fun x => c) a + s.indicator (fun x => c') a) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c c' : E
⊢ indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')

Tactic:
simp_rw [indicatorConstLp, ← MemLp.toLp_add, indicator_add]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c c' : E
⊢ MemLp.toLp ((s.indicator fun x => c) + s.indicator fun x => c') ⋯ =
    MemLp.toLp (fun a => s.indicator (fun x => c) a + s.indicator (fun x => c') a) ⋯
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_sub_zsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]
    (f : F) (x : G) (n : ℤ) : f (x - n • a) = f x - n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℤ
⊢ f (x - n • a) = f x - n • b

Tactic:
simpa [sub_eq_add_neg] using map_add_zsmul f x (-n)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.mul_right_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q ≠ 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥

Tactic:
refine ⟨hq, ?_⟩

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬p.degree = ⊥

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0

Tactic:
rw [Ne, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or,
  degree_eq_bot]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬p.degree = ⊥

Tactic:
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
⊢ p * q ≠ 0

Tactic:
by_cases h : p = 1

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ⊥ < 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0

Tactic:
simpa [h]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥

Tactic:
refine (lt_trans ?_ h).ne'

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ⊥ < 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem getD_map (f : α → β) (x : α) (o : Option α) :
  (o.map f).getD (f x) = f (getD o x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x : α
o : Option α
⊢ (Option.map f o).getD (f x) = f (o.getD x)

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots.le_of_dvd (h : q ≠ 0) : p ∣ q → roots p ≤ roots q

Proof state:
case intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ p.roots ≤ (p * k).roots

Tactic:
exact Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : q ≠ 0
⊢ p ∣ q → p.roots ≤ q.roots

Tactic:
rintro ⟨k, rfl⟩

Result:
case intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p k : R[X]
h : p * k ≠ 0
⊢ p.roots ≤ (p * k).roots
-- Mathlib/Data/Set/Card.lean
theorem ncard_insert_eq_ite {a : α} [Decidable (a ∈ s)] (hs : s.Finite

Proof state:
case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam s.Finite _auto✝
h : a ∈ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
rw [ncard_insert_of_mem h, if_pos h]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam s.Finite _auto✝
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam s.Finite _auto✝
h : a ∈ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam s.Finite _auto✝
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Proof state:
case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam s.Finite _auto✝
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
rw [ncard_insert_of_not_mem h hs, if_neg h]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation.map_add_le_max' (x y : R) :
    v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
⊢ x ∈ v.asIdeal ^ nmin

Tactic:
rw [← Associates.le_singleton_iff x nmin _,
  Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
⊢ Irreducible (Associates.mk v.asIdeal)
-- Mathlib/Algebra/GeomSum.lean
theorem Nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
    ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range n, a / b ^ i) * (b - 1) ≤ a * b

Tactic:
rcases n with - | n

Result:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b

case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b

Proof state:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)

Tactic:
refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_

Result:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range n, a / b ^ i) * (b - 1) ≤ a * b

Proof state:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b

Tactic:
rw [mul_comm]

Result:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b

Proof state:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b

Tactic:
exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

Result:
no goals

Proof state:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b

Tactic:
rw [sum_range_zero, zero_mul]

Result:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.mul [NonUnitalCommSemiring R] {s₁ s₂ : R}
    (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ * s₂)

Proof state:
R : Type u_1
inst✝ : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ s₂ ∈ NonUnitalSubsemiring.sumSq R

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ s₁ ∈ NonUnitalSubsemiring.sumSq R

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ * s₂)

Tactic:
simpa using mul_mem (by simpa : _ ∈ NonUnitalSubsemiring.sumSq R) (by simpa)

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma map_comp {i j k : Fin 2} (hij : i ≤ j) (hjk : j ≤ k) :
    map f i k (hij.trans hjk) = map f i j hij ≫ map f j k hjk

Proof state:
case inr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
⊢ map f i j ⋯ = map f i j hij ≫ map f j j hjk

Tactic:
rw [map_id, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk

Tactic:
obtain rfl | rfl : i = j ∨ j = k := by omega

Result:
case inl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
⊢ map f i k ⋯ = map f i i hij ≫ map f i k hjk

case inr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
⊢ map f i j ⋯ = map f i j hij ≫ map f j j hjk

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
⊢ i = j ∨ j = k

Tactic:
omega

Result:
no goals

Proof state:
case inl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
⊢ map f i k ⋯ = map f i i hij ≫ map f i k hjk

Tactic:
rw [map_id, id_comp]

Result:
no goals
-- Mathlib/Order/CountableDenseLinearOrder.lean
lemma exists_orderEmbedding_insert [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β]
    [nonem : Nonempty β]  (S : Finset α) (f : S ↪o β) (a : α) :
    ∃ (g : (insert a S : Finset α) ↪o β),
      g ∘ (Set.inclusion ((S.subset_insert a) : ↑S ⊆ ↑(insert a S))) = f

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
y : β
hy : ∃ a_1, a < a_1 ∧ ∃ (x : a_1 ∈ S), f ⟨a_1, ⋯⟩ = y
w✝¹ : α
hx : w✝¹ < a
w✝ : w✝¹ ∈ S
⊢ f ⟨w✝¹, ⋯⟩ < y

Tactic:
obtain ⟨_, hy, _, rfl⟩ := hy

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : { x // x ∈ S } ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => ↑x < a) S.attach)
Sgt : Finset β := Finset.image (⇑f) (Finset.filter (fun x => a < ↑x) S.attach)
w✝³ : α
hx : w✝³ < a
w✝² : w✝³ ∈ S
w✝¹ : α
hy : a < w✝¹
w✝ : w✝¹ ∈ S
⊢ f ⟨w✝³, ⋯⟩ < f ⟨w✝¹, ⋯⟩
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem mul_inv_of_eq {a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ a * ↑u⁻¹ = 1

Tactic:
rw [← h, u.mul_inv]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
lemma concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    ConcaveOn ℝ≥0 univ fun x : ℝ≥0 ↦ x ^ p

Proof state:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p

Tactic:
rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)

Result:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ 0

case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p

Proof state:
case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p

Tactic:
exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

Result:
no goals

Proof state:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ 1

Tactic:
simpa only [rpow_one] using concaveOn_id convex_univ

Result:
no goals

Proof state:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ 0

Tactic:
simpa only [rpow_zero] using concaveOn_const (c := 1) convex_univ

Result:
no goals

Proof state:
case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p

Tactic:
rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)

Result:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ 1

case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
-- Mathlib/Order/Filter/Prod.lean
theorem map_prod (m : α × β → γ) (f : Filter α) (g : Filter β) :
    map m (f ×ˢ g) = (f.map fun a b => m (a, b)).seq g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ ∀ (s : Set γ), (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
intro s

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Proof state:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = (map (fun a b => m (a, b)) f).seq g

Tactic:
simp only [Filter.ext_iff, mem_map, mem_prod_iff, mem_map_seq_iff, exists_and_left]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ ∀ (s : Set γ), (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s
-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_natCast : ∀ n : ℕ, ⟦(n : PGame)⟧ = (n : Game)
  | 0 => rfl
  | n + 1 => by
    rw [PGame.nat_succ, quot_add, Nat.cast_add, Nat.cast_one, quot_natCast]
    rfl

Proof state:
n : ℕ
⊢ ↑n + ⟦1⟧ = ↑n + 1

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ ⟦↑(n + 1)⟧ = ↑(n + 1)

Tactic:
rw [PGame.nat_succ, quot_add, Nat.cast_add, Nat.cast_one, quot_natCast]

Result:
n : ℕ
⊢ ↑n + ⟦1⟧ = ↑n + 1
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_induction (f s : ℕ → β) (base : s 0 = 1)
    (step : ∀ n, s (n + 1) = s n * f n) (n : ℕ) :
    ∏ k ∈ Finset.range n, f k = s n

Proof state:
case zero
β : Type u_4
inst✝ : CommMonoid β
f s : ℕ → β
base : s 0 = 1
step : ∀ (n : ℕ), s (n + 1) = s n * f n
⊢ ∏ k ∈ range 0, f k = s 0

Tactic:
rw [Finset.prod_range_zero, base]

Result:
no goals

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f s : ℕ → β
base : s 0 = 1
step : ∀ (n : ℕ), s (n + 1) = s n * f n
n : ℕ
⊢ ∏ k ∈ range n, f k = s n

Tactic:
induction n with
| zero => rw [Finset.prod_range_zero, base]
| succ k hk => simp only [hk, Finset.prod_range_succ, step, mul_comm]

Result:
no goals

Proof state:
case succ
β : Type u_4
inst✝ : CommMonoid β
f s : ℕ → β
base : s 0 = 1
step : ∀ (n : ℕ), s (n + 1) = s n * f n
k : ℕ
hk : ∏ k ∈ range k, f k = s k
⊢ ∏ k ∈ range (k + 1), f k = s (k + 1)

Tactic:
simp only [hk, Finset.prod_range_succ, step, mul_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Constructions.lean
theorem Pi.nnnorm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (π i)] {i : ι} (y : π i) :
    ‖Pi.single i y‖₊ = ‖y‖₊

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
⊢ ∀ (b : ι), ‖single i y b‖₊ = single i ‖y‖₊ b

Tactic:
intro b

Result:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
b : ι
⊢ ‖single i y b‖₊ = single i ‖y‖₊ b

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
H : ∀ (b : ι), ‖single i y b‖₊ = single i ‖y‖₊ b
⊢ ‖single i y‖₊ = ‖y‖₊

Tactic:
simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
⊢ ‖single i y‖₊ = ‖y‖₊

Tactic:
have H : ∀ b, ‖single i y b‖₊ = single (f := fun _ ↦ ℝ≥0) i ‖y‖₊ b := by
  intro b
  refine Pi.apply_single (fun i (x : π i) ↦ ‖x‖₊) ?_ i y b
  simp

Result:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
H : ∀ (b : ι), ‖single i y b‖₊ = single i ‖y‖₊ b
⊢ ‖single i y‖₊ = ‖y‖₊

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
b : ι
⊢ ∀ (i : ι), (fun i x => ‖x‖₊) i 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
b : ι
⊢ ‖single i y b‖₊ = single i ‖y‖₊ b

Tactic:
refine Pi.apply_single (fun i (x : π i) ↦ ‖x‖₊) ?_ i y b

Result:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
b : ι
⊢ ∀ (i : ι), (fun i x => ‖x‖₊) i 0 = 0
-- Mathlib/RingTheory/Jacobson/Ring.lean
lemma isJacobsonRing_of_finiteType {A B : Type*} [CommRing A] [CommRing B]
    [Algebra A B] [IsJacobsonRing A] [Algebra.FiniteType A B] : IsJacobsonRing B

Proof state:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsJacobsonRing A
inst✝ : Algebra.FiniteType A B
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι A →ₐ[A] B
hf : Function.Surjective ⇑f
⊢ IsJacobsonRing B

Tactic:
exact isJacobsonRing_of_surjective ⟨f.toRingHom, hf⟩

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsJacobsonRing A
inst✝ : Algebra.FiniteType A B
⊢ IsJacobsonRing B

Tactic:
obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›

Result:
case intro.intro.intro
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsJacobsonRing A
inst✝ : Algebra.FiniteType A B
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι A →ₐ[A] B
hf : Function.Surjective ⇑f
⊢ IsJacobsonRing B
-- Mathlib/Data/Finsupp/Order.lean
@[simp] lemma single_le_single : single i a ≤ single i b ↔ a ≤ b

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a b : α
⊢ single i a ≤ single i b ↔ a ≤ b

Tactic:
exact Pi.single_le_single

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a b : α
⊢ single i a ≤ single i b ↔ a ≤ b

Tactic:
classical exact Pi.single_le_single

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.left_of_add_measure {f : α → β} (h : Integrable f (μ + ν)) : Integrable f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 μ

Tactic:
exact h.left_of_add_measure

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f (μ + ν)
⊢ Integrable f μ

Tactic:
rw [← memLp_one_iff_integrable] at h ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 μ