harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/Different.lean
/-- If `b` is an `A`-integral basis of `L` with discriminant `b`, then `d • a * x` is integral over
  `A` for all `a ∈ I` and `x ∈ Iᵛ`. -/
lemma isIntegral_discr_mul_of_mem_traceDual
    (I : Submodule B L) {ι} [DecidableEq ι] [Fintype ι]
    {b : Basis ι K L} (hb : ∀ i, IsIntegral A (b i))
    {a x : L} (ha : a ∈ I) (hx : x ∈ Iᵛ) :
    IsIntegral A ((discr K b) • a * x)

Proof state:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Field L
inst✝¹³ : Algebra A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)
this : Function.Injective (traceMatrix K ⇑b).mulVec
i : ι
a✝ : i ∈ Finset.univ
⊢ IsIntegral A (b.equivFun (discr K ⇑b • a * x) i • b i)

Tactic:
rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def]

Result:
case h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Field L
inst✝¹³ : Algebra A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)
this : Function.Injective (traceMatrix K ⇑b).mulVec
i : ι
a✝ : i ∈ Finset.univ
⊢ IsIntegral A ((algebraMap K L) ((traceMatrix K ⇑b).cramer (fun i => (Algebra.trace K L) (x * a * b i)) i) * b i)
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem c_mul_im_sq_le_normSq_denom : (g 1 0 * z.im) ^ 2 ≤ Complex.normSq (denom g z)

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
d : ℝ := ↑↑g 1 1
⊢ (↑↑g 1 0 * z.im) ^ 2 + (↑↑g 1 0 * z.re + ↑↑g 1 1) ^ 2 =
    (↑↑g 1 0 * z.re - 0 * z.im + ↑↑g 1 1) * (↑↑g 1 0 * z.re - 0 * z.im + ↑↑g 1 1) +
      (↑↑g 1 0 * z.im + 0 * z.re + 0) * (↑↑g 1 0 * z.im + 0 * z.re + 0)

Tactic:
ring

Result:
no goals

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
d : ℝ := ↑↑g 1 1
⊢ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 = Complex.normSq (denom g z)

Tactic:
dsimp [c, d, denom, Complex.normSq]

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
d : ℝ := ↑↑g 1 1
⊢ (↑↑g 1 0 * z.im) ^ 2 + (↑↑g 1 0 * z.re + ↑↑g 1 1) ^ 2 =
    (↑↑g 1 0 * z.re - 0 * z.im + ↑↑g 1 1) * (↑↑g 1 0 * z.re - 0 * z.im + ↑↑g 1 1) +
      (↑↑g 1 0 * z.im + 0 * z.re + 0) * (↑↑g 1 0 * z.im + 0 * z.re + 0)

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (↑↑g 1 0 * z.im) ^ 2 ≤ Complex.normSq (denom g z)

Tactic:
set c := g 1 0

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g z)

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
d : ℝ := ↑↑g 1 1
⊢ (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2

Tactic:
nlinarith

Result:
no goals

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g z)

Tactic:
set d := g 1 1

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
d : ℝ := ↑↑g 1 1
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g z)

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
c : ℝ := ↑↑g 1 0
d : ℝ := ↑↑g 1 1
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g z)

Tactic:
calc
  (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
  _ = Complex.normSq (denom g z) := by dsimp [c, d, denom, Complex.normSq]; ring

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem compContinuousLinearMap_applyComposition {n : ℕ} (p : FormalMultilinearSeries 𝕜 F G)
    (f : E →L[𝕜] F) (c : Composition n) (v : Fin n → E) :
    (p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (f ∘ v)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 F G
f : E →L[𝕜] F
c : Composition n
v : Fin n → E
⊢ (fun i => (p (c.blocksFun i)) (⇑f ∘ v ∘ ⇑(c.embedding i))) = fun i =>
    (p (c.blocksFun i)) ((⇑f ∘ v) ∘ ⇑(c.embedding i))

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 F G
f : E →L[𝕜] F
c : Composition n
v : Fin n → E
⊢ (p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (⇑f ∘ v)

Tactic:
simp (config := {unfoldPartialApp := true}) [applyComposition]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 F G
f : E →L[𝕜] F
c : Composition n
v : Fin n → E
⊢ (fun i => (p (c.blocksFun i)) (⇑f ∘ v ∘ ⇑(c.embedding i))) = fun i =>
    (p (c.blocksFun i)) ((⇑f ∘ v) ∘ ⇑(c.embedding i))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_modify_ne (f g : α → α) {m n} (l : List α) (h : m ≠ n) :
    (modify f m l).modify g n = (l.modify g n).modify f m

Proof state:
case h
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
m' : Nat
h₁ : m' < (modify g n (modify f m l)).length
h₂ : m' < (modify f m (modify g n l)).length
⊢ (modify g n (modify f m l))[m'] = (modify f m (modify g n l))[m']

Tactic:
simp only [getElem_modify, getElem_modify_ne, h₂]

Result:
case h
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
m' : Nat
h₁ : m' < (modify g n (modify f m l)).length
h₂ : m' < (modify f m (modify g n l)).length
⊢ (if n = m' then g (if m = m' then f l[m'] else l[m']) else if m = m' then f l[m'] else l[m']) =
    if m = m' then f (if n = m' then g l[m'] else l[m']) else if n = m' then g l[m'] else l[m']

Proof state:
case h.isFalse.isFalse
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
m' : Nat
h₁ : m' < (modify g n (modify f m l)).length
h₂ : m' < (modify f m (modify g n l)).length
h✝¹ : ¬n = m'
h✝ : ¬m = m'
⊢ l[m'] = l[m']

Tactic:
rfl

Result:
no goals

Proof state:
case h.isTrue.isTrue
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
m' : Nat
h₁ : m' < (modify g n (modify f m l)).length
h₂ : m' < (modify f m (modify g n l)).length
h✝¹ : n = m'
h✝ : m = m'
⊢ g (f l[m']) = f (g l[m'])

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
m' : Nat
h₁ : m' < (modify g n (modify f m l)).length
h₂ : m' < (modify f m (modify g n l)).length
⊢ (if n = m' then g (if m = m' then f l[m'] else l[m']) else if m = m' then f l[m'] else l[m']) =
    if m = m' then f (if n = m' then g l[m'] else l[m']) else if n = m' then g l[m'] else l[m']

Tactic:
split <;> split <;> first | rfl | omega

Result:
no goals

Proof state:
case hl
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ (modify g n (modify f m l)).length = (modify f m (modify g n l)).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ modify g n (modify f m l) = modify f m (modify g n l)

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ (modify g n (modify f m l)).length = (modify f m (modify g n l)).length

case h
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ ∀ (i : Nat) (h₁ : i < (modify g n (modify f m l)).length) (h₂ : i < (modify f m (modify g n l)).length),
    (modify g n (modify f m l))[i] = (modify f m (modify g n l))[i]

Proof state:
case h
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ ∀ (i : Nat) (h₁ : i < (modify g n (modify f m l)).length) (h₂ : i < (modify f m (modify g n l)).length),
    (modify g n (modify f m l))[i] = (modify f m (modify g n l))[i]

Tactic:
intro m' h₁ h₂

Result:
case h
α : Type u_1
f g : α → α
m n : Nat
l : List α
h : m ≠ n
m' : Nat
h₁ : m' < (modify g n (modify f m l)).length
h₂ : m' < (modify f m (modify g n l)).length
⊢ (modify g n (modify f m l))[m'] = (modify f m (modify g n l))[m']
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.sum {ι : Type*} {f : ι → E → F} {s : Finset ι}
    (h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) : ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) univ
⊢ ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) univ

Tactic:
exact ContDiffOn.sum h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x
⊢ ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x

Tactic:
simp only [← contDiffOn_univ] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) univ
⊢ ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) univ
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem map_apply {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
    v.map f s = v (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑(v.map f) s = ↑v (f ⁻¹' s)

Tactic:
rw [map, dif_pos hf]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      s =
    ↑v (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      s =
    ↑v (f ⁻¹' s)

Tactic:
exact if_pos hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem all_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : all n f = all m (fun i h => f i (by omega))

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
i : Nat
h : i < m
⊢ i < n

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
⊢ n.all f = m.all fun i h => f i ⋯

Tactic:
subst m

Result:
n : Nat
f : (i : Nat) → i < n → Bool
⊢ n.all f = n.all fun i h => f i ⋯

Proof state:
n : Nat
f : (i : Nat) → i < n → Bool
⊢ n.all f = n.all fun i h => f i ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edgeSet_fromEdgeSet : (fromEdgeSet s).edgeSet = s \ { e | e.IsDiag }

Proof state:
case h
V : Type u
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ {e | e.IsDiag}

Tactic:
exact Sym2.ind (by simp) e

Result:
no goals

Proof state:
V : Type u
s : Set (Sym2 V)
e : Sym2 V
⊢ ∀ (x y : V), s(x, y) ∈ (fromEdgeSet s).edgeSet ↔ s(x, y) ∈ s \ {e | e.IsDiag}

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
s : Set (Sym2 V)
⊢ (fromEdgeSet s).edgeSet = s \ {e | e.IsDiag}

Tactic:
ext e

Result:
case h
V : Type u
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ {e | e.IsDiag}
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_update_segment (i : ι) (x₁ x₂ : π i) (y : ∀ i, π i) :
    update y i '' [x₁ -[𝕜] x₂] = [update y i x₁ -[𝕜] update y i x₂]

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ (fun x => update y i (x.1 • x₁ + x.2 • x₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • update y i x₁ + p.2 • update y i x₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Result:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
⊢ update y i (a.1 • x₁ + a.2 • x₂) = a.1 • update y i x₁ + a.2 • update y i x₂

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ update y i '' [x₁-[𝕜]x₂] = [update y i x₁-[𝕜]update y i x₂]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]

Result:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ (fun x => update y i (x.1 • x₁ + x.2 • x₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • update y i x₁ + p.2 • update y i x₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
⊢ update y i (a.1 • x₁ + a.2 • x₂) = a.1 • update y i x₁ + a.2 • update y i x₂

Tactic:
simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp]
lemma inner_smul_right_real {z : ℝ} {x y : E} : ⟪x, z • y⟫ = z • ⟪x, y⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ inner x (z •> y) = z •> inner x y

Tactic:
rw [h₁, ← star_inner, inner_smul_left_complex]

Result:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ star (star ↑z •> inner y x) = z •> inner x y

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> y = ↑z •> y

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ star (star ↑z •> inner y x) = z •> inner x y

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
⊢ inner x (z •> y) = z •> inner x y

Tactic:
have h₁ : z • y = (z : ℂ) • y := by simp

Result:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ inner x (z •> y) = z •> inner x y
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integral_fn_integral_add_comp ⦃f g : γ → E⦄ (F : E → E')
    (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
    ∫ x, F (∫ y, f y + g y ∂η x) ∂κ a = ∫ x, F (∫ y, f y ∂η x + ∫ y, g y ∂η x) ∂κ a

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y + g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ + ∫ (y : γ), g y ∂η a✝)

Tactic:
simp [integral_add h2f h2g]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ (fun x => F (∫ (y : γ), f y + g y ∂η x)) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f y ∂η x + ∫ (y : γ), g y ∂η x)

Tactic:
filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y + g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ + ∫ (y : γ), g y ∂η a✝)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫ (x : β), F (∫ (y : γ), f y + g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x + ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
refine integral_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ (fun x => F (∫ (y : γ), f y + g y ∂η x)) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f y ∂η x + ∫ (y : γ), g y ∂η x)
-- Mathlib/RingTheory/RingHom/FinitePresentation.lean
theorem finitePresentation_isStableUnderBaseChange :
    IsStableUnderBaseChange @FinitePresentation

Proof state:
case h.e'_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.FinitePresentation R T
this : Algebra.FinitePresentation S (S ⊗[R] T)
e_4✝ : CommSemiring.toSemiring = Algebra.TensorProduct.instSemiring
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := Algebra.TensorProduct.includeLeftRingHom.toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
simp_rw [Algebra.smul_def]

Result:
case h.e'_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.FinitePresentation R T
this : Algebra.FinitePresentation S (S ⊗[R] T)
e_4✝ : CommSemiring.toSemiring = Algebra.TensorProduct.instSemiring
r✝ : S
x✝ : S ⊗[R] T
⊢ (algebraMap S (S ⊗[R] T)) r✝ * x✝ = (algebraMap S (S ⊗[R] T)) r✝ * x✝
-- Mathlib/Data/Complex/Exponential.lean
theorem norm_exp_sub_one_sub_id_le {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖exp x - 1 - x‖ ≤ ‖x‖ ^ 2 :=
  calc
    ‖exp x - 1 - x‖ = ‖exp x - ∑ m ∈ range 2, x ^ m / m.factorial‖

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 * 1 = ‖x‖ ^ 2

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 * (↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹) ≤ ‖x‖ ^ 2 * 1

Tactic:
gcongr

Result:
case h
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹ ≤ 1

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1 - x‖ = ‖cexp x - ∑ m ∈ range 2, x ^ m / ↑m.factorial‖

Tactic:
simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc, Nat.factorial]

Result:
no goals

Proof state:
case h
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹ ≤ 1

Tactic:
norm_num [Nat.factorial]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/List.lean
/-- Product of elements of a list `l` equals zero if and only if `0 ∈ l`. See also
`List.prod_eq_zero` for an implication that needs weaker typeclass assumptions. -/
@[simp] lemma prod_eq_zero_iff : ∀ {l : List M₀}, l.prod = 0 ↔ (0 : M₀) ∈ l
  | [] => by simp
  | a :: l => by rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

Proof state:
M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ [].prod = 0 ↔ 0 ∈ []

Tactic:
simp

Result:
no goals

Proof state:
M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l

Tactic:
rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

Result:
no goals