harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma mapEq_trans {i₁ i₂ i₃ : K} (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) {h₃ : i₃ ≤ x}
    (m₁₂ : MapEq F G i₁ i₂ h₁₂ (h₂₃.trans h₃)) (m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃) :
    MapEq F G i₁ i₃ (h₁₂.trans h₂₃) h₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ ∃ (hX : F.obj ⟨i₁, ⋯⟩ = G.obj ⟨i₁, ⋯⟩) (hY : F.obj ⟨i₃, h₃⟩ = G.obj ⟨i₃, h₃⟩),
    F.map (homOfLE ⋯) = eqToHom hX ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom ⋯

Tactic:
simp [-homOfLE_comp, m₁₂.w, m₂₃.w]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯

Tactic:
rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ MapEq F G i₁ i₃ ⋯ h₃

Tactic:
simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ ∃ (hX : F.obj ⟨i₁, ⋯⟩ = G.obj ⟨i₁, ⋯⟩) (hY : F.obj ⟨i₃, h₃⟩ = G.obj ⟨i₃, h₃⟩),
    F.map (homOfLE ⋯) = eqToHom hX ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem allM_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
    v.toArray.allM p = v.allM p

Proof state:
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
v : Vector α n
⊢ Array.allM p v.toArray = allM p v

Tactic:
cases v

Result:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.allM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    allM p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.allM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    allM p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem hlast' (i : Fin N.succ) (h : 1 ≤ τ) : a.r (last N) ≤ τ * a.r i

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
rw [this]

Result:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r (last N)

Proof state:
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
rcases lt_or_le i (last N) with (H | H)

Result:
case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : i < last N
⊢ a.r (last N) ≤ τ * a.r i

case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
⊢ a.r (last N) ≤ τ * a.r i

Proof state:
case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : i < last N
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
exact (a.hlast i H).2

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r (last N)

Tactic:
exact le_mul_of_one_le_left (a.rpos _).le h

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
have : i = last N := top_le_iff.1 H

Result:
case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r i
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem leadingCoeff_of_single {a : Γ} {r : R} : leadingCoeff (single a r) = r

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).leadingCoeff = r

Tactic:
simp only [leadingCoeff, single_eq_zero_iff]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ (if h : (single a) r = 0 then 0 else ((single a) r).coeff (⋯.min ⋯)) = r

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ (if h : (single a) r = 0 then 0 else ((single a) r).coeff (⋯.min ⋯)) = r

Tactic:
by_cases h : r = 0 <;> simp [h]

Result:
no goals
-- Mathlib/Data/Nat/Size.lean
theorem size_eq_bits_len (n : ℕ) : n.bits.length = n.size

Proof state:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (bit b✝ n✝).bits.length = (bit b✝ n✝).size

Tactic:
rw [size_bit, bits_append_bit _ _ h]

Result:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (b✝ :: n✝.bits).length = n✝.size.succ

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0

Proof state:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ bit b✝ n✝ ≠ 0

Tactic:
simpa [bit_eq_zero_iff]

Result:
no goals

Proof state:
case z

⊢ (bits 0).length = size 0

Tactic:
simp

Result:
no goals

Proof state:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
ih : n✝.bits.length = n✝.size
⊢ (b✝ :: n✝.bits).length = n✝.size.succ

Tactic:
simp [ih]

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

Proof state:
α : Type u_1
as bs : Array α
⊢ as.reverse = bs ↔ as = bs.reverse

Tactic:
constructor <;> (rintro rfl; simp)

Result:
no goals

Proof state:
case mpr
α : Type u_1
as bs : Array α
⊢ as = bs.reverse → as.reverse = bs

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
bs : Array α
⊢ bs.reverse.reverse = bs

Proof state:
case mpr
α : Type u_1
bs : Array α
⊢ bs.reverse.reverse = bs

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_differentiableWithinAt_iff {f : G → E} {s : Set G} {x : G} :
    DifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
⊢ DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
refine
  ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (⇑iso.symm ∘ ⇑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
  iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (⇑iso.symm ∘ ⇑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_pow_mul {n : ℕ} : X ^ n * p = p * X ^ n

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ (n + 1) * p = p * X ^ (n + 1)

Tactic:
conv_lhs => rw [pow_succ]

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ (n + 1)

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ X ^ 0 * p = p * X ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ (n + 1)

Tactic:
rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ X ^ n * p = p * X ^ n

Tactic:
induction n with
| zero => simp
| succ n ih =>
  conv_lhs => rw [pow_succ]
  rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
theorem image_specComap_zeroLocus_eq_zeroLocus_comap (hf : Surjective f) (I : Ideal S) :
    f.specComap '' zeroLocus I = zeroLocus (I.comap f)

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ f.specComap x = p

Tactic:
refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩

Result:
case refine_2.refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ f.specComap { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem mkContinuousMultilinear_norm_le' (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
    ‖mkContinuousMultilinear f C H‖ ≤ max C 0

Proof state:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖f.mkContinuousMultilinear C H‖ ≤ C ⊔ 0

Tactic:
dsimp only [mkContinuousMultilinear]

Result:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖{ toFun := fun m => (f m).mkContinuous (C * ∏ i : ι, ‖m i‖) ⋯, map_update_add' := ⋯,
            map_update_smul' := ⋯ }.mkContinuous
        (C ⊔ 0) ⋯‖ ≤
    C ⊔ 0

Proof state:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖{ toFun := fun m => (f m).mkContinuous (C * ∏ i : ι, ‖m i‖) ⋯, map_update_add' := ⋯,
            map_update_smul' := ⋯ }.mkContinuous
        (C ⊔ 0) ⋯‖ ≤
    C ⊔ 0

Tactic:
exact mkContinuous_norm_le _ (le_max_right _ _) _

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finrank_pos_iff [NoZeroSMulDivisors R M] :
    0 < finrank R M ↔ Nontrivial M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < finrank R M ↔ 0 < ↑(finrank R M)

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank]

Result:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < finrank R M ↔ 0 < ↑(finrank R M)
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma opProdIsoCoprod_inv_inl : (opProdIsoCoprod A B).inv.unop ≫ coprod.inl.unop = prod.fst

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).inv.unop ≫ coprod.inl.unop = prod.fst

Tactic:
rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
theorem iSup_succ [SuccOrder α] (x : α) : ⨆ a : Iio x, succ a.1 = x

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
⊢ ∀ (i : ↑(Iio x)), succ ↑i ≤ x

Tactic:
exact fun a ↦ succ_le_of_lt a.2

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x

Tactic:
rw [ciSup_le_iff' H]

Result:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
⊢ ∀ (i : ↑(Iio x)), succ ↑i ≤ x

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ ⨆ a, succ ↑a = x

Tactic:
have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
  ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩

Result:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
⊢ ⨆ a, succ ↑a = x

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ succ x ∈ upperBounds (range fun a => succ ↑a)

Tactic:
simp +contextual [upperBounds, succ_le_succ, le_of_lt]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i

Tactic:
exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a

Tactic:
rw [lt_ciSup_iff' H]

Result:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i

Proof state:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
⊢ ⨆ a, succ ↑a = x

Tactic:
apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)

Result:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x

α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a => succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_succ_column_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :
    det A = ∑ i : Fin n.succ, (-1) ^ (i : ℕ) * A i 0 * det (A.submatrix i.succAbove Fin.succ)

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j => A (i.succ.succAbove i_1) j.succ).det

Tactic:
rw [Fin.val_succ, pow_succ', this, mul_assoc, mul_assoc, mul_left_comm (ε _),
  ← det_permute, Matrix.det_apply, Finset.mul_sum, Finset.mul_sum]

Result:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x =
    ∑ i_1 : Perm (Fin n),
      -1 *
        (A i.succ 0 *
          sign i_1 •
            ∏ i_2 : Fin n, (of fun i_3 j => A (i.succ.succAbove i_3) j.succ).submatrix (⇑i.cycleRange) id (i_1 i_2) i_2)

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ sign (decomposeFin.symm (i.succ, σ)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ •
          ∏ i_1 : Fin n, (of fun i_2 j => A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)

Tactic:
rw [Equiv.Perm.decomposeFin.symm_sign, if_neg (Fin.succ_ne_zero i)]

Result:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * sign σ) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ •
          ∏ i_1 : Fin n, (of fun i_2 j => A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
theorem Integrable.integral_norm_condKernel {f : α × Ω → F} (hf_int : Integrable f ρ) :
    Integrable (fun x ↦ ∫ y, ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

Tactic:
have hf_ae : AEStronglyMeasurable f ρ := hf_int.1

Result:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
    Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

Tactic:
exact hf_int.2

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

Tactic:
rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int

Result:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
    Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem map_bind₁ (f : R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    map f (bind₁ g φ) = bind₁ (fun i : σ => (map f) (g i)) (map f φ)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (eval₂Hom C fun i => (map f) (g i)) ((map f) φ) = (bind₁ fun i => (map f) (g i)) ((map f) φ)

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (map f) ((bind₁ g) φ) = (bind₁ fun i => (map f) (g i)) ((map f) φ)

Tactic:
rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (eval₂Hom C fun i => (map f) (g i)) ((map f) φ) = (bind₁ fun i => (map f) (g i)) ((map f) φ)