harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 ⦋n⦌

Proof state:
case a.h.h.h
n : ℕ
i : Fin (n + 1)
j : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ i.succ ≫ σ i)) j) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) j)

Tactic:
rcases i with ⟨i, _⟩

Result:
case a.h.h.h.mk
n : ℕ
j : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, isLt✝⟩.succ ≫ σ ⟨i, isLt✝⟩)) j) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) j)

Proof state:
case a.h.h.h.mk.mk
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j

Tactic:
split_ifs <;> simp <;> simp at * <;> omega

Result:
no goals

Proof state:
case a.h.h.h.mk.mk
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, isLt✝¹⟩.succ ≫ σ ⟨i, isLt✝¹⟩)) ⟨j, isLt✝⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, isLt✝⟩)

Tactic:
dsimp [δ, σ, Fin.succAbove, Fin.predAbove]

Result:
case a.h.h.h.mk.mk
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j

Proof state:
case a.h.h.h.mk
n : ℕ
j : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, isLt✝⟩.succ ≫ σ ⟨i, isLt✝⟩)) j) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) j)

Tactic:
rcases j with ⟨j, _⟩

Result:
case a.h.h.h.mk.mk
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, isLt✝¹⟩.succ ≫ σ ⟨i, isLt✝¹⟩)) ⟨j, isLt✝⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, isLt✝⟩)

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌

Tactic:
ext j

Result:
case a.h.h.h
n : ℕ
i : Fin (n + 1)
j : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ i.succ ≫ σ i)) j) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) j)
-- Mathlib/Data/Complex/Basic.lean
/-- The inequality `s × t ⊆ s₁ × t₁` holds in `ℂ` iff it holds in `ℝ × ℝ`. -/
lemma reProdIm_subset_iff {s s₁ t t₁ : Set ℝ} : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Proof state:
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
rw [← @preimage_equivRealProd_prod s t, ← @preimage_equivRealProd_prod s₁ t₁]

Result:
s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Proof state:
s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact Equiv.preimage_subset equivRealProd _ _

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
theorem DirichletCharacter.LSeries_eulerProduct {N : ℕ} (χ : DirichletCharacter ℂ N)
    (hs : 1 < s.re) :
    Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - χ p * (p : ℂ) ^ (-s))⁻¹) atTop
      (𝓝 (L ↗χ s))

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (L (fun n => χ ↑n) s))

Tactic:
rw [← tsum_dirichletSummand χ hs]

Result:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))

Tactic:
apply eulerProduct_completely_multiplicative <| summable_dirichletSummand χ hs

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticWithinAt.comp {g : F → G} {f : E → F} {x : E} {t : Set F} {s : Set E}
    (hg : AnalyticWithinAt 𝕜 g t (f x)) (hf : AnalyticWithinAt 𝕜 f s x) (h : Set.MapsTo f s t) :
    AnalyticWithinAt 𝕜 (g ∘ f) s x

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
g : F → G
f : E → F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
_p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f _p s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
exact (hq.comp hp h).analyticWithinAt

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
g : F → G
f : E → F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
let ⟨_q, hq⟩ := hg

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
g : F → G
f : E → F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

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
g : F → G
f : E → F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
let ⟨_p, hp⟩ := hf

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
g : F → G
f : E → F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
_p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f _p s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib/SetTheory/Game/Impartial.lean
theorem nonneg : ¬G < 0

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ ¬G < 0

Tactic:
simpa using nonpos (-G)

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Pi.lean
theorem piFamily_add (f g : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    piFamily (f + g) = piFamily f + piFamily g

Proof state:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (f + g)) x✝¹ x✝ = (piFamily f + piFamily g) x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
⊢ piFamily (f + g) = piFamily f + piFamily g

Tactic:
ext

Result:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (f + g)) x✝¹ x✝ = (piFamily f + piFamily g) x✝¹ x✝
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_transpose [Zero α] (v : n → α) : (diagonal v)ᵀ = diagonal v

Proof state:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
by_cases h : i = j

Result:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Proof state:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
simp [h, transpose]

Result:
no goals

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
⊢ (diagonal v)ᵀ = diagonal v

Tactic:
ext i j

Result:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j

Proof state:
case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
simp [h, transpose, diagonal_apply_ne' _ h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
@[simp] lemma natDegree_X_pow_mul (hp : p ≠ 0) : natDegree (X ^ n * p) = natDegree p + n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (X ^ n * p).natDegree = p.natDegree + n

Tactic:
rw [commute_X_pow, natDegree_mul_X_pow n hp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma degree_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0

Tactic:
simpa [ha.mul_left_eq_zero]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (p * C a).degree = p.degree

Tactic:
rw [degree_mul', degree_C ha.ne_zero]

Result:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.degree + 0 = p.degree

R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).degree = p.degree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
⊢ (0 * C a).degree = degree 0

case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (p * C a).degree = p.degree

Proof state:
case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (p * C a).degree = p.degree

Tactic:
nontriviality R

Result:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (p * C a).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.degree + 0 = p.degree

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
⊢ (0 * C a).degree = degree 0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem two_lt_lineCount [Finite P] [Finite L] (p : P) : 2 < lineCount L p

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ 2 < lineCount L p

Tactic:
simpa only [lineCount_eq L p, Nat.succ_lt_succ_iff] using one_lt_order P L

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem toCone_isLeast : IsLeast { t : ConvexCone 𝕜 E | s ⊆ t } (hs.toCone s)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
t : ConvexCone 𝕜 E
ht : t ∈ {t | s ⊆ ↑t}
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
hx : c • y ∈ toCone s hs
⊢ c • y ∈ t

Tactic:
exact t.smul_mem hc (ht hy)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ IsLeast {t | s ⊆ ↑t} (toCone s hs)

Tactic:
refine ⟨hs.subset_toCone, fun t ht x hx => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
t : ConvexCone 𝕜 E
ht : t ∈ {t | s ⊆ ↑t}
x : E
hx : x ∈ toCone s hs
⊢ x ∈ t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
t : ConvexCone 𝕜 E
ht : t ∈ {t | s ⊆ ↑t}
x : E
hx : x ∈ toCone s hs
⊢ x ∈ t

Tactic:
rcases hs.mem_toCone.1 hx with ⟨c, hc, y, hy, rfl⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
t : ConvexCone 𝕜 E
ht : t ∈ {t | s ⊆ ↑t}
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
hx : c • y ∈ toCone s hs
⊢ c • y ∈ t
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@[reassoc (attr := simp)]
lemma map_comp_map_s (φ : W.LeftFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    φ.map L hL ≫ L.map φ.s = L.map φ.f

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ φ.map L hL ≫ L.map φ.s = L.map φ.f

Tactic:
letI := hL _ φ.hs

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map φ.s) := hL φ.s φ.hs
⊢ φ.map L hL ≫ L.map φ.s = L.map φ.f

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map φ.s) := hL φ.s φ.hs
⊢ φ.map L hL ≫ L.map φ.s = L.map φ.f

Tactic:
simp [map]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, we have that `λ ^ 2` divides one amongst `S'.a + S'.b`,
`S'.a + η * S'.b` and `S'.a + η ^ 2 * S'.b`. -/
lemma lambda_sq_dvd_or_dvd_or_dvd :
    λ ^ 2 ∣ S'.a + S'.b ∨ λ ^ 2 ∣ S'.a + η * S'.b ∨ λ ^ 2 ∣ S'.a + η ^ 2 * S'.b

Proof state:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
have := (pow_dvd_pow_of_dvd (lambda_sq_dvd_c S') 3).mul_left S'.u

Result:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this : (λ ^ 2) ^ 3 ∣ ↑S'.u * S'.c ^ 3
⊢ False

Proof state:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2

Result:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_smul [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F]
    (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜)
    (f : α → E) : setToFun μ T hT (c • f) = c • setToFun μ T hT f

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
by_cases hr : c = 0

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f μ
hr : c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hf : ¬Integrable f μ
hr : ¬c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
-- Mathlib/Topology/SeparatedMap.lean
theorem IsSeparatedMap.pullback {f : X → Y} (sep : IsSeparatedMap f) (g : A → Y) :
    IsSeparatedMap (@snd X Y A f g)

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → Y
⊢ IsSeparatedMap snd

Tactic:
rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢

Result:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → Y
⊢ IsClosed (Function.pullbackDiagonal snd)

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → Y
⊢ IsClosed (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)

Tactic:
refine sep.preimage (Continuous.mapPullback ?_ ?_) <;>
apply_rules [continuous_fst, continuous_subtype_val, Continuous.comp]

Result:
no goals

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → Y
⊢ IsClosed (Function.pullbackDiagonal snd)

Tactic:
rw [← preimage_map_fst_pullbackDiagonal]

Result:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → Y
⊢ IsClosed (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)
-- Mathlib/Topology/Constructions.lean
theorem isClosed_range_inl : IsClosed (range (inl : X → X ⊕ Y))

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosed (range inl)

Tactic:
rw [← isOpen_compl_iff, compl_range_inl]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen (range inr)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen (range inr)

Tactic:
exact isOpen_range_inr

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma ciSup_or' (p q : Prop) (f : p ∨ q → α) :
    ⨆ (h : p ∨ q), f h = (⨆ h : p, f (.inl h)) ⊔ ⨆ h : q, f (.inr h)

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
⊢ ⨆ (h : p ∨ q), f h = (⨆ (h : p), f ⋯) ⊔ ⨆ (h : q), f ⋯

Tactic:
by_cases hp : p <;>
by_cases hq : q <;>
simp [hp, hq]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_piecewise_ite' [∀ x, Decidable (x ∈ t)]
    (h : ContinuousOn f (s ∩ closure t)) (h' : ContinuousOn g (s' ∩ closure tᶜ))
    (H : s ∩ frontier t = s' ∩ frontier t) (Heq : EqOn f g (s ∩ frontier t)) :
    ContinuousOn (t.piecewise f g) (t.ite s s')

Proof state:
case ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a

Tactic:
rwa [ite_inter_of_inter_eq _ H]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn (t.piecewise f g) (t.ite s s')

Tactic:
apply ContinuousOn.piecewise

Result:
case ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a

case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn f (t.ite s s' ∩ closure t)

case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (t.ite s s' ∩ closure tᶜ)

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn f (t.ite s s' ∩ closure t)

Tactic:
rwa [ite_inter_closure_eq_of_inter_frontier_eq H]

Result:
no goals

Proof state:
case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn g (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (t.ite s s' ∩ closure tᶜ)

Tactic:
rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]

Result:
no goals