harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem leftCoset_eq_iff {x y : α} : x • (s : Set α) = y • s ↔ x⁻¹ * y ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
exact s.mul_mem_cancel_left h

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ x⁻¹ * y ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s

case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s

Tactic:
rw [Set.ext_iff]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x • ↑s ↔ x_1 ∈ y • ↑s) ↔ x⁻¹ * y ∈ s

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ x⁻¹ * y ∈ s

Tactic:
apply (h y).mpr

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ y⁻¹ * y ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
rw [← mul_inv_cancel_right x⁻¹ y]

Result:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s

Tactic:
exact s.one_mem

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ y⁻¹ * y ∈ s

Tactic:
rw [inv_mul_cancel]

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
rw [mul_assoc]

Result:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x • ↑s ↔ x_1 ∈ y • ↑s) ↔ x⁻¹ * y ∈ s

Tactic:
simp_rw [mem_leftCoset_iff, SetLike.mem_coe]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

Tactic:
intro h z

Result:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_mem (w : σ → M) (φ : MvPolynomial σ R) (m : M) :
    weightedHomogeneousComponent w m φ ∈ weightedHomogeneousSubmodule R w m

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w m) φ) m

Tactic:
exact weightedHomogeneousComponent_isWeightedHomogeneous m φ

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ (weightedHomogeneousComponent w m) φ ∈ weightedHomogeneousSubmodule R w m

Tactic:
rw [mem_weightedHomogeneousSubmodule]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w m) φ) m
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_zero_measure (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂(0 : Measure α) = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂0 = 0

Tactic:
simp [laverage]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem seq_seq {s : Set (β → γ)} {t : Set (α → β)} {u : Set α} :
    seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ image2 (fun f a => f a) s (image2 (fun f a => f a) t u) =
    image2 (fun f a => f a) (image2 (fun x1 x2 => x1 ∘ x2) s t) u

Tactic:
exact .symm <| image2_assoc fun _ _ _ ↦ rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ s.seq (t.seq u) = (((fun x1 x2 => x1 ∘ x2) '' s).seq t).seq u

Tactic:
simp only [seq_eq_image2, image2_image_left]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ image2 (fun f a => f a) s (image2 (fun f a => f a) t u) =
    image2 (fun f a => f a) (image2 (fun x1 x2 => x1 ∘ x2) s t) u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem resolve_left_dvd₂ (a c d p x : Int)
    (h₁ : p ≤ a * x) (h₃ : d ∣ c * x + s) :
    a * d ∣ c * resolve_left a c d p x + c * p + a * s

Proof state:
case mk.h
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d / ↑((a * d).gcd c) ∣ ↑(a.lcm (a * d / ↑((a * d).gcd c)))

Tactic:
exact Int.dvd_lcm_right

Result:
no goals

Proof state:
case mk
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d ∣ c * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + c * p + a * s

Tactic:
simp only [Int.add_assoc, ofNat_emod]

Result:
case mk
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d ∣ c * (↑k' % ↑(a.lcm (a * d / ↑((a * d).gcd c)))) + (c * p + a * s)

Proof state:
case mk.w.intro
s a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
z : Int
r : c * x + s = d * z
⊢ a * d ∣ c * ↑k' + (c * p + a * s)

Tactic:
refine ⟨z, ?_⟩

Result:
case mk.w.intro
s a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
z : Int
r : c * x + s = d * z
⊢ c * ↑k' + (c * p + a * s) = a * d * z

Proof state:
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
⊢ a * d ∣ c * resolve_left a c d p x + c * p + a * s

Tactic:
simp only [h₁, resolve_left_eq, resolve_left']

Result:
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
⊢ a * d ∣ c * ↑((add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))) + c * p + a * s

Proof state:
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
⊢ a * d ∣ c * ↑((add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))) + c * p + a * s

Tactic:
obtain ⟨k', w⟩ := add_of_le h₁

Result:
case mk
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d ∣ c * ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + c * p + a * s

Proof state:
case mk.w.intro
s a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
z : Int
r : c * x + s = d * z
⊢ c * ↑k' + (c * p + a * s) = a * d * z

Tactic:
rw [Int.mul_assoc, ← r, Int.mul_add, Int.mul_comm c x, ← Int.mul_assoc, w, Int.add_mul,
  Int.mul_comm c, Int.mul_comm c, ← Int.add_assoc, Int.add_comm (p * c)]

Result:
no goals

Proof state:
case mk
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d ∣ c * (↑k' % ↑(a.lcm (a * d / ↑((a * d).gcd c)))) + (c * p + a * s)

Tactic:
apply dvd_mul_emod_add_of_dvd_mul_add

Result:
case mk.w
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d ∣ c * ↑k' + (c * p + a * s)

case mk.h
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d / ↑((a * d).gcd c) ∣ ↑(a.lcm (a * d / ↑((a * d).gcd c)))

Proof state:
case mk.w
s a c d p x : Int
h₁ : p ≤ a * x
h₃ : d ∣ c * x + s
k' : Nat
w : a * x = p + ↑k'
⊢ a * d ∣ c * ↑k' + (c * p + a * s)

Tactic:
obtain ⟨z, r⟩ := h₃

Result:
case mk.w.intro
s a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
z : Int
r : c * x + s = d * z
⊢ a * d ∣ c * ↑k' + (c * p + a * s)
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.lt_on_open_segment' (hf : StrictConvexOn 𝕜 s f) {x y : E} (hx : x ∈ s)
    (hy : y ∈ s) (hxy : x ≠ y) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
    f (a • x + b • y) < max (f x) (f y) :=
  calc
    f (a • x + b • y) < a • f x + b • f y := hf.2 hx hy hxy ha hb hab
    _ ≤ a • max (f x) (f y) + b • max (f x) (f y)

Proof state:
case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ f x ⊔ f y

Tactic:
apply le_max_right

Result:
no goals

Proof state:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ f x ⊔ f y

Tactic:
apply le_max_left

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • (f x ⊔ f y) + b • (f x ⊔ f y)

Tactic:
gcongr

Result:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ f x ⊔ f y

case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ f x ⊔ f y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertList_of_contains_eq_true [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (contains : containsKey k toInsert = true) :
    getEntry? k (insertList l toInsert) = getEntry? k toInsert

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
contains : containsKey k toInsert = true
⊢ getEntry? k (insertList l toInsert) = getEntry? k toInsert

Tactic:
rw [getEntry?_insertList distinct_l distinct_toInsert]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
contains : containsKey k toInsert = true
⊢ (getEntry? k toInsert).or (getEntry? k l) = getEntry? k toInsert

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
contains : containsKey k toInsert = true
⊢ (getEntry? k toInsert).or (getEntry? k l) = getEntry? k toInsert

Tactic:
rw [containsKey_eq_isSome_getEntry?] at contains

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
contains : (getEntry? k toInsert).isSome = true
⊢ (getEntry? k toInsert).or (getEntry? k l) = getEntry? k toInsert

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
contains : (getEntry? k toInsert).isSome = true
⊢ (getEntry? k toInsert).or (getEntry? k l) = getEntry? k toInsert

Tactic:
exact Option.or_of_isSome contains

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma fwdDiff_choose (j : ℕ) : Δ_[1] (fun x ↦ x.choose (j + 1) : ℕ → ℤ) = fun x ↦ x.choose j

Proof state:
j : ℕ
⊢ (Δ_[1] fun x => ↑(x.choose (j + 1))) = fun x => ↑(x.choose j)

Tactic:
ext n

Result:
case h
j n : ℕ
⊢ Δ_[1] (fun x => ↑(x.choose (j + 1))) n = ↑(n.choose j)

Proof state:
case h
j n : ℕ
⊢ Δ_[1] (fun x => ↑(x.choose (j + 1))) n = ↑(n.choose j)

Tactic:
simp only [fwdDiff, choose_succ_succ' n j, cast_add, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem SeminormFamily.finset_sup_comp (q : SeminormFamily 𝕜₂ F ι) (s : Finset ι)
    (f : E →ₛₗ[σ₁₂] F) : (s.sup q).comp f = s.sup (q.comp f)

Proof state:
case h
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(s.sup fun i => ⟨(q i) (f x), ⋯⟩) = ↑(s.sup fun i => ⟨(q.comp f i) x, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ((s.sup q).comp f) x = (s.sup (q.comp f)) x

Tactic:
rw [Seminorm.comp_apply, Seminorm.finset_sup_apply, Seminorm.finset_sup_apply]

Result:
case h
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(s.sup fun i => ⟨(q i) (f x), ⋯⟩) = ↑(s.sup fun i => ⟨(q.comp f i) x, ⋯⟩)

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
⊢ (s.sup q).comp f = s.sup (q.comp f)

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ((s.sup q).comp f) x = (s.sup (q.comp f)) x
-- Mathlib/Data/Stream/Init.lean
theorem get_drop (n m : ℕ) (s : Stream' α) : get (drop m s) n = get s (m + n)

Proof state:
α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (m + n)

Tactic:
rw [Nat.add_comm]

Result:
α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (n + m)

Proof state:
α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (n + m)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem mul_add (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ :=
  ext fun n => by
    classical simp only [coeff_mul, mul_add, Finset.sum_add_distrib, LinearMap.map_add]

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ₁ * (φ₂ + φ₃)) = (coeff R n) (φ₁ * φ₂ + φ₁ * φ₃)

Tactic:
classical simp only [coeff_mul, mul_add, Finset.sum_add_distrib, LinearMap.map_add]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ₁ * (φ₂ + φ₃)) = (coeff R n) (φ₁ * φ₂ + φ₁ * φ₃)

Tactic:
simp only [coeff_mul, mul_add, Finset.sum_add_distrib, LinearMap.map_add]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasStrictFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) :
    HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0

Proof state:
case h.e'_12.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
x : 𝔸
⊢ 1 x = ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)) x

Tactic:
change x = expSeries 𝕂 𝔸 1 fun _ => x

Result:
case h.e'_12.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
x : 𝔸
⊢ x = (expSeries 𝕂 𝔸 1) fun x_1 => x

Proof state:
case h.e'_12.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
x : 𝔸
⊢ x = (expSeries 𝕂 𝔸 1) fun x_1 => x

Tactic:
simp [expSeries_apply_eq, Nat.factorial]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
⊢ HasStrictFDerivAt (exp 𝕂) 1 0

Tactic:
convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt

Result:
case h.e'_12
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
⊢ 1 = (continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)

Proof state:
case h.e'_12
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
⊢ 1 = (continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)

Tactic:
ext x

Result:
case h.e'_12.h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
h : 0 < (expSeries 𝕂 𝔸).radius
x : 𝔸
⊢ 1 x = ((continuousMultilinearCurryFin1 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 1)) x
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem qsmul_eq_C_mul (a : ℚ) (f : R[X]) : a • f = Polynomial.C (a : R) * f

Proof state:
R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = C ↑a * f

Tactic:
rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem norm_sub_eq_add_norm_iff_angle_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)

Tactic:
calc
  ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 := by linarith
  _ = -(‖x‖ * ‖y‖) := by ring

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π

Tactic:
refine ⟨fun h => ?_, norm_sub_eq_add_norm_of_angle_eq_pi⟩

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
⊢ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)

Tactic:
obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2

Tactic:
linarith

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 = -(‖x‖ * ‖y‖)

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
⊢ angle x y = π

Tactic:
rw [← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)

Tactic:
rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_sub_pow_two_real] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunction_injective (h1 : 0 < c) (h2 : c < 1 / 2) :
    Function.Injective (cantorFunction c)

Proof state:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
⊢ f = g

Tactic:
ext

Result:
case h
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
x✝ : ℕ
⊢ f x✝ = g x✝

Proof state:
case false.h
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ cantorFunction c f < cantorFunction c g

Tactic:
refine increasing_cantorFunction h1 h2 hn fn ?_

Result:
case false.h
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ g n = true

Proof state:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ f k = g k

Tactic:
apply of_not_not

Result:
case a
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ ¬¬f k = g k

Proof state:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ ∀ k < n, f k = g k

Tactic:
intro k hk

Result:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ f k = g k