harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
protected lemma IsNested.nest : p.nest.IsNested := ⟨nest_ne_zero, fun i lb ub ↦ by
  simp_rw [nest, length_append, length_singleton] at ub ⊢
  rw [take_append_of_le_length (by rw [singleton_append, length_cons]; omega),
    take_append_eq_append_take, take_of_length_le (by rw [length_singleton]; omega),
    length_singleton, singleton_append, count_cons_of_ne (by simp), count_cons_self,
    Nat.lt_add_one_iff]
  exact p.count_D_le_count_U _⟩

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ ([U] ++ ↑p).length

Tactic:
rw [singleton_append, length_cons]

Result:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ (↑p).length + 1

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ [U].length ≤ i

Tactic:
rw [length_singleton]

Result:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ 1 ≤ i

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ 1 ≤ i

Tactic:
omega

Result:
no goals

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ D ≠ U

Tactic:
simp

Result:
no goals

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))

Tactic:
rw [take_append_of_le_length (by rw [singleton_append, length_cons]; omega),
  take_append_eq_append_take, take_of_length_le (by rw [length_singleton]; omega),
  length_singleton, singleton_append, count_cons_of_ne (by simp), count_cons_self,
  Nat.lt_add_one_iff]

Result:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) ≤ count U (List.take (i - 1) ↑p)

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) ≤ count U (List.take (i - 1) ↑p)

Tactic:
exact p.count_D_le_count_U _

Result:
no goals

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < (↑p.nest).length
⊢ count D (List.take i ↑p.nest) < count U (List.take i ↑p.nest)

Tactic:
simp_rw [nest, length_append, length_singleton] at ub ⊢

Result:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))

Proof state:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ (↑p).length + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem LinearOrder.convexOn_of_lt (hs : Convex 𝕜 s)
    (hf : ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 →
      f (a • x + b • y) ≤ a • f x + b • f y) :
    ConvexOn 𝕜 s f

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : b + a = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃x : E⦄,
          x ∈ s →
            ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) →
        ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → x < y → f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
⊢ f (b • y + a • x) ≤ b • f y + a • f x

Tactic:
exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h)

Result:
no goals

Proof state:
𝕜✝ : Type u_1
E✝ : Type u_2
β✝ : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜✝
inst✝¹⁰ : AddCommMonoid E✝
inst✝⁹ : OrderedAddCommMonoid β✝
inst✝⁸ : Module 𝕜✝ E✝
inst✝⁷ : Module 𝕜✝ β✝
inst✝⁶ : LinearOrder E✝
s✝ : Set E✝
f✝ : E✝ → β✝
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : x < y
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
exact hf hx hy h ha hb hab

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall (g : F →L[𝕜] G)
    (h : HasFiniteFPowerSeriesOnBall f p x n r) :
    HasFiniteFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x n r :=
  ⟨g.comp_hasFPowerSeriesOnBall h.1, fun m hm ↦ by
    rw [compFormalMultilinearSeries_apply, h.finite m hm]
    ext; exact map_zero g⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
⊢ g.compFormalMultilinearSeries p m = 0

Tactic:
rw [compFormalMultilinearSeries_apply, h.finite m hm]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
⊢ g.compContinuousMultilinearMap 0 = 0

Proof state:
case H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
x✝ : Fin m → E
⊢ (g.compContinuousMultilinearMap 0) x✝ = 0 x✝

Tactic:
exact map_zero g

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
⊢ g.compContinuousMultilinearMap 0 = 0

Tactic:
ext

Result:
case H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
x✝ : Fin m → E
⊢ (g.compContinuousMultilinearMap 0) x✝ = 0 x✝
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Submartingale.stoppedValue_leastGE_eLpNorm_le [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hr : 0 ≤ r) (hf0 : f 0 = 0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
    eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + R)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (x : Ω), stoppedValue f (leastGE f r i) x ∂μ

Tactic:
rw [← setIntegral_univ]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (x : Ω) in Set.univ, stoppedValue f (leastGE f r i) x ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (x : Ω) in Set.univ, stoppedValue f (leastGE f r i) x ∂μ

Tactic:
refine le_trans ?_ ((hf.stoppedValue_leastGE r).setIntegral_le (zero_le _) MeasurableSet.univ)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (ω : Ω) in Set.univ, stoppedValue f (leastGE f r 0) ω ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (ω : Ω) in Set.univ, stoppedValue f (leastGE f r 0) ω ∂μ

Tactic:
simp_rw [stoppedValue, leastGE, hitting_of_le le_rfl, hf0, integral_zero', le_rfl]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R)

Tactic:
refine eLpNorm_one_le_of_le' ((hf.stoppedValue_leastGE r).integrable _) ?_
  (norm_stoppedValue_leastGE_le hr hf0 hbdd i)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 0 ≤ ∫ (x : Ω), stoppedValue f (leastGE f r i) x ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_zip_left :
    ∀ {l₁ : List α} {l₂ : List β}, length l₁ ≤ length l₂ → (unzip (zip l₁ l₂)).1 = l₁
  | [], _, _ => rfl
  | _, [], h => by rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]; rfl
  | _ :: _, _ :: _, h => by
    simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]

Proof state:
α : Type u_1
β : Type u_2
x✝ : List α
h : x✝.length ≤ [].length
⊢ (x✝.zip []).unzip.fst = x✝

Tactic:
rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]

Result:
α : Type u_1
β : Type u_2
x✝ : List α
h : x✝.length ≤ [].length
⊢ ([].zip []).unzip.fst = []

Proof state:
α : Type u_1
β : Type u_2
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
h : (head✝¹ :: tail✝¹).length ≤ (head✝ :: tail✝).length
⊢ ((head✝¹ :: tail✝¹).zip (head✝ :: tail✝)).unzip.fst = head✝¹ :: tail✝¹

Tactic:
simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝ : List α
h : x✝.length ≤ [].length
⊢ ([].zip []).unzip.fst = []

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem IsPowMul.restriction {R S : Type*} [NormedCommRing R] [CommRing S] [Algebra R S]
    (A : Subalgebra R S) {f : S → ℝ} (hf_pm : IsPowMul f) :
    IsPowMul fun x : A => f x.val := fun x n hn => by
  simpa [SubsemiringClass.coe_pow] using hf_pm (↑x) hn

Proof state:
R : Type u_5
S : Type u_6
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A : Subalgebra R S
f : S → ℝ
hf_pm : IsPowMul f
x : ↥A
n : ℕ
hn : 1 ≤ n
⊢ (fun x => f ↑x) (x ^ n) = (fun x => f ↑x) x ^ n

Tactic:
simpa [SubsemiringClass.coe_pow] using hf_pm (↑x) hn

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma image_op_pow (s : Finset α) : ∀ n : ℕ, (s ^ n).image op = s.image op ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => by rw [pow_succ, pow_succ', image_op_mul, image_op_pow]

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ', image_op_mul, image_op_pow]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ image op (s ^ 0) = image op s ^ 0

Tactic:
simp [singleton_one]

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

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

Tactic:
exact Set.image_const_add_Ioo _ _ _

Result:
no goals

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

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

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_filter (s : Multiset α) (p : α → Prop) [DecidablePred p] :
    Multiset.toFinset (s.filter p) = s.toFinset.filter p

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter p s.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter p s).toFinset = Finset.filter p s.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter p s.toFinset
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem sup_toSubfield (S T : IntermediateField F E) :
    (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Subfield.closure (Set.range ⇑(algebraMap F E) ∪ (↑S ∪ ↑T)) = Subfield.closure (↑S ∪ ↑T)

Tactic:
congr 1

Result:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Set.range ⇑(algebraMap F E) ∪ (↑S ∪ ↑T) = ↑S ∪ ↑T

Proof state:
case e_s.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
x : F
⊢ (algebraMap F E) x ∈ ↑S ∪ ↑T

Tactic:
exact Set.mem_union_left _ (algebraMap_mem S x)

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

Tactic:
rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ (S ⊔ T).toSubfield = Subfield.closure (↑S.toSubfield ∪ ↑T.toSubfield)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ (S ⊔ T).toSubfield = Subfield.closure (↑S.toSubfield ∪ ↑T.toSubfield)

Tactic:
simp_rw [sup_def, adjoin_toSubfield, coe_toSubfield]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Subfield.closure (Set.range ⇑(algebraMap F E) ∪ (↑S ∪ ↑T)) = Subfield.closure (↑S ∪ ↑T)

Proof state:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑S ∪ ↑T

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case e_s.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
x : F
⊢ (algebraMap F E) x ∈ ↑S ∪ ↑T

Proof state:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Set.range ⇑(algebraMap F E) ∪ (↑S ∪ ↑T) = ↑S ∪ ↑T

Tactic:
rw [Set.union_eq_right]

Result:
case e_s
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑S ∪ ↑T
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem _root_.LinearIsometryEquiv.piLpCongrLeft_single [DecidableEq ι] [DecidableEq ι']
    (e : ι ≃ ι') (i : ι) (v : E) :
    LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e ((WithLp.equiv p (_ → E)).symm <| Pi.single i v) =
      (WithLp.equiv p (_ → E)).symm (Pi.single (e i) v)

Proof state:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring 𝕜
ι' : Type u_5
inst✝⁴ : Fintype ι'
E : Type u_6
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
⊢ (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) =
    (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v)

Tactic:
funext x

Result:
case h
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring 𝕜
ι' : Type u_5
inst✝⁴ : Fintype ι'
E : Type u_6
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
x : ι'
⊢ (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) x =
    (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v) x

Proof state:
case h
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring 𝕜
ι' : Type u_5
inst✝⁴ : Fintype ι'
E : Type u_6
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
x : ι'
⊢ (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) x =
    (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v) x

Tactic:
simp [LinearIsometryEquiv.piLpCongrLeft_apply, LinearEquiv.piCongrLeft', Equiv.piCongrLeft',
  Pi.single, Function.update, Equiv.symm_apply_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem mul_invOf_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible b
⊢ a * b * ⅟b = a

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Defs.lean
@[to_additive]
lemma prod_induction
    (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ l, p x) :
    p l.prod

Proof state:
case nil
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ [] → p x
⊢ p [].prod

Tactic:
simpa

Result:
no goals

Proof state:
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod

Tactic:
induction l with
| nil => simpa
| cons a l ih =>
  rw [List.prod_cons]
  simp only [mem_cons, forall_eq_or_imp] at base
  exact hom _ _ (base.1) (ih base.2)

Result:
no goals

Proof state:
case cons
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a * l.prod)

Tactic:
simp only [mem_cons, forall_eq_or_imp] at base

Result:
case cons
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)

Proof state:
case cons
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod

Tactic:
rw [List.prod_cons]

Result:
case cons
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a * l.prod)

Proof state:
case cons
M : Type u_4
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)

Tactic:
exact hom _ _ (base.1) (ih base.2)

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem nsmul_congr {a a' : ℕ} (_ : (a : ℕ) = a') (_ : b = b') (_ : a' • b' = c) :
    (a • (b : R)) = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b b' c : R
a a' : ℕ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
b' : R
a' : ℕ
⊢ a' • b' = a' • b'

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b' : R
a' : ℕ
⊢ a' • b' = a' • b'

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem natCast_div_le (m n : ℕ) :
    (m / n : ℕ) ≤ (m : EReal) / (n : EReal)

Proof state:
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
exact Nat.cast_div_le

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary **rearrangement inequality**. -/
lemma mul_add_mul_le_mul_add_mul [ExistsAddOfLE α] [MulPosMono α]
    [AddLeftMono α] [AddLeftReflectLE α]
    (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c d : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hcd : c ≤ d
b : α
hab : a ≤ a + b
⊢ a * d + (a + b) * c ≤ a * c + (a + b) * d

Tactic:
obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd

Result:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
b : α
hab : a ≤ a + b
d : α
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * (c + d) + (a + b) * c ≤ a * c + (a + b) * (c + d)

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
obtain ⟨b, rfl⟩ := exists_add_of_le hab

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c d : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hcd : c ≤ d
b : α
hab : a ≤ a + b
⊢ a * d + (a + b) * c ≤ a * c + (a + b) * d

Proof state:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
b : α
hab : a ≤ a + b
d : α
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * c + (a + b) * c + a * d ≤ a * c + (a + b) * c + (a + b) * d

Tactic:
exact add_le_add_left (mul_le_mul_of_nonneg_right hab hd) _

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
b : α
hab : a ≤ a + b
d : α
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * (c + d) + (a + b) * c ≤ a * c + (a + b) * (c + d)

Tactic:
rw [mul_add, add_right_comm, mul_add, ← add_assoc]

Result:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
b : α
hab : a ≤ a + b
d : α
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * c + (a + b) * c + a * d ≤ a * c + (a + b) * c + (a + b) * d