harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Enriched/Basic.lean
theorem e_assoc' (W X Y Z : C) :
    (α_ _ _ _).hom ≫ _ ◁ eComp V X Y Z ≫ eComp V W X Z =
      eComp V W X Y ▷ _ ≫ eComp V W Y Z

Proof state:
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C : Type u₁
inst✝ : EnrichedCategory V C
W X Y Z : C
⊢ (α_ (EnrichedCategory.Hom W X) (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z)).hom ≫
      EnrichedCategory.Hom W X ◁ eComp V X Y Z ≫ eComp V W X Z =
    eComp V W X Y ▷ EnrichedCategory.Hom Y Z ≫ eComp V W Y Z

Tactic:
rw [← e_assoc V W X Y Z, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem nonempty_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Nonempty

Proof state:
α : Type u_1
hs : ∅.ncard ≠ 0
⊢ False

Tactic:
simp at hs

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
α : Type u_1
hs : ∅.ncard ≠ 0
⊢ False

Proof state:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Result:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIso.inv_fst :
    (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ i₁ ≫ pullback.fst _ _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    fst i₁ i₂ ≫ i₁ ≫ fst f i

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫
      fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    fst i₁ i₂ ≫ i₁ ≫ fst f i

Tactic:
delta pullbackDiagonalMapIso

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    fst i₁ i₂ ≫ i₁ ≫ fst f i
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem algEquivOfAssociated_apply_root {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    algEquivOfAssociated hp hpq (root p) = root q

Proof state:
K : Type u_1
inst✝ : Field K
p q : K[X]
hp : p ≠ 0
hpq : Associated p q
⊢ (algEquivOfAssociated hp hpq) (root p) = root q

Tactic:
rw [← coe_algHom, algEquivOfAssociated_toAlgHom, liftHom_root]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem mem_leftTransversals_iff_existsUnique_inv_mul_mem :
    S ∈ leftTransversals T ↔ ∀ g : G, ∃! s : S, (s : G)⁻¹ * g ∈ T

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
g : G
⊢ ∃! s, (↑s)⁻¹ * g ∈ T

Tactic:
obtain ⟨x, h1, h2⟩ := h g

Result:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
g : G
x : ↑S × ↑T
h1 : ↑x.1 * ↑x.2 = g
h2 : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! s, (↑s)⁻¹ * g ∈ T

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ S ∈ leftTransversals T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T

Tactic:
rw [leftTransversals, Set.mem_setOf_eq, isComplement_iff_existsUnique]

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ (∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g) ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
refine ⟨⟨x, (↑x)⁻¹ * g, h1⟩, mul_inv_cancel_left (↑x) g, fun y hy => ?_⟩

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
y : ↑S × ↑T
hy : (fun x => ↑x.1 * ↑x.2 = g) y
⊢ y = (x, ⟨(↑x)⁻¹ * g, h1⟩)

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
y : ↑S × ↑T
hy : (fun x => ↑x.1 * ↑x.2 = g) y
hf : y.1 = x
⊢ y = (x, ⟨(↑x)⁻¹ * g, h1⟩)

Tactic:
exact Prod.ext hf (Subtype.ext (eq_inv_mul_of_mul_eq (hf ▸ hy)))

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ (∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g) ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T

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

Result:
case refine_1
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
g : G
⊢ ∃! s, (↑s)⁻¹ * g ∈ T

case refine_2
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
obtain ⟨x, h1, h2⟩ := h g

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_update_smul [DecidableEq ι] (i : ι) (c : R) (u : s i →ₗ[R] t i) :
    map (update f i (c • u)) = c • map (update f i u)

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
c : R
u : s i →ₗ[R] t i
⊢ map (update f i (c • u)) = c • map (update f i u)

Tactic:
ext x

Result:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
c : R
u : s i →ₗ[R] t i
x : (i : ι) → s i
⊢ ((map (update f i (c • u))).compMultilinearMap (tprod R)) x =
    ((c • map (update f i u)).compMultilinearMap (tprod R)) x

Proof state:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
c : R
u : s i →ₗ[R] t i
x : (i : ι) → s i
⊢ ((map (update f i (c • u))).compMultilinearMap (tprod R)) x =
    ((c • map (update f i u)).compMultilinearMap (tprod R)) x

Tactic:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.smul_apply,
  MultilinearMap.map_update_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_changeForm (x : CliffordAlgebra Q) :
    changeForm h' (changeForm h x) = changeForm (changeForm.add_proof h h') x

Proof state:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) (x✝ + y✝)) = (changeForm ⋯) (x✝ + y✝)

Tactic:
rw [map_add, map_add, map_add, hx, hy]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm h') ((changeForm h) x) = (changeForm ⋯) x

Tactic:
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [changeForm_algebraMap]
| add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
| ι_mul _ _ hx => rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
    LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
    add_comm (_ : CliffordAlgebra Q'')]

Result:
no goals

Proof state:
case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
r✝ : R
⊢ (changeForm h') ((changeForm h) ((algebraMap R (CliffordAlgebra Q)) r✝)) =
    (changeForm ⋯) ((algebraMap R (CliffordAlgebra Q)) r✝)

Tactic:
simp_rw [changeForm_algebraMap]

Result:
no goals

Proof state:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (changeForm h') ((changeForm h) ((ι Q) m✝ * x✝)) = (changeForm ⋯) ((ι Q) m✝ * x✝)

Tactic:
rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
add_comm (_ : CliffordAlgebra Q'')]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- Basis elements have strictly monotone degree. -/
lemma basis_degree_strictMono : StrictMono <| degree ∘ (S.basis hCoeff) := fun _ _  ↦ by simp

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
x✝¹ x✝ : ℕ
⊢ x✝¹ < x✝ → (degree ∘ ⇑(S.basis hCoeff)) x✝¹ < (degree ∘ ⇑(S.basis hCoeff)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep.comp' {ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep <| t ∘ f)
    (hf : Surjective f) : iSupIndep t

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
⊢ iSupIndep t

Tactic:
intro i

Result:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Proof state:
case intro
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ j, ⨆ (_ : j ≠ f i'), t j)

Tactic:
rw [← hf.iSup_comp]

Result:
case intro
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ x, ⨆ (_ : f x ≠ f i'), t (f x))

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
obtain ⟨i', rfl⟩ := hf i

Result:
case intro
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ j, ⨆ (_ : j ≠ f i'), t j)

Proof state:
case intro
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ x, ⨆ (_ : f x ≠ f i'), t (f x))

Tactic:
exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reflBEq_iff [BEq α] : ReflBEq (List α) ↔ ReflBEq α

Proof state:
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (List α) ↔ ReflBEq α

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (List α) → ReflBEq α

case mpr
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq α → ReflBEq (List α)

Proof state:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
a : List α
⊢ (a == a) = true

Tactic:
induction a with
| nil => simp only [List.instBEq, List.beq]
| cons a as ih =>
  simp [List.instBEq, List.beq]
  exact ih

Result:
no goals

Proof state:
case mpr.refl.cons
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
a : α
as : List α
ih : (as == as) = true
⊢ as.beq as = true

Tactic:
exact ih

Result:
no goals

Proof state:
case mpr.refl.nil
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ([] == []) = true

Tactic:
simp only [List.instBEq, List.beq]

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq α → ReflBEq (List α)

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ReflBEq (List α)

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
⊢ ReflBEq α

Tactic:
constructor

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
⊢ ∀ {a : α}, (a == a) = true

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ReflBEq (List α)

Tactic:
constructor

Result:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ∀ {a : List α}, (a == a) = true

Proof state:
case mpr.refl.cons
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
a : α
as : List α
ih : (as == as) = true
⊢ (a :: as == a :: as) = true

Tactic:
simp [List.instBEq, List.beq]

Result:
case mpr.refl.cons
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
a : α
as : List α
ih : (as == as) = true
⊢ as.beq as = true

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
a : α
⊢ (a == a) = true

Tactic:
suffices ([a] == [a]) = true by
  simpa only [List.instBEq, List.beq, Bool.and_true]

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
a : α
⊢ ([a] == [a]) = true

Proof state:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
⊢ ∀ {a : List α}, (a == a) = true

Tactic:
intro a

Result:
case mpr.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq α
a : List α
⊢ (a == a) = true

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
⊢ ∀ {a : α}, (a == a) = true

Tactic:
intro a

Result:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
a : α
⊢ (a == a) = true

Proof state:
case mp.refl
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
a : α
⊢ ([a] == [a]) = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
a : α
this : ([a] == [a]) = true
⊢ (a == a) = true

Tactic:
simpa only [List.instBEq, List.beq, Bool.and_true]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
⊢ ReflBEq (List α) → ReflBEq α

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : BEq α
h : ReflBEq (List α)
⊢ ReflBEq α
-- Mathlib/Topology/IndicatorConstPointwise.lean
/-- The indicator functions of `Asᵢ` evaluated at `x` tend to the indicator function of `A`
evaluated at `x` if and only if we eventually have the equivalence `x ∈ Asᵢ ↔ x ∈ A`. -/
@[simp] lemma tendsto_indicator_const_apply_iff_eventually [T1Space β] (b : β) [NeZero b]
    (x : α) :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b) x) L (𝓝 (A.indicator (fun (_ : α) ↦ b) x))
      ↔ ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A)

Proof state:
case nhd_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {b}ᶜ ∈ 𝓝 0

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]

Result:
no goals

Proof state:
case nhd_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {0}ᶜ ∈ 𝓝 b

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]

Result:
no goals

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
apply tendsto_indicator_const_apply_iff_eventually' _ b

Result:
case nhd_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {0}ᶜ ∈ 𝓝 b

case nhd_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {b}ᶜ ∈ 𝓝 0
-- Mathlib/Data/Set/Sups.lean
theorem lowerClosure_infs [SemilatticeInf α] (s t : Set α) :
    lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t

Proof state:
case a.h
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)

Tactic:
simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs, exists_and_left, exists_prop,
  LowerSet.coe_sup, Set.mem_inter_iff]

Result:
case a.h
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t

Proof state:
case a.h.mpr
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2

Tactic:
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩

Result:
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1

Proof state:
case a.h
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t

Tactic:
constructor

Result:
case a.h.mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t

case a.h.mpr
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2

Proof state:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
⊢ lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t

Tactic:
ext a

Result:
case a.h
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)

Proof state:
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1

Tactic:
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩

Result:
no goals

Proof state:
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t

Tactic:
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩

Result:
no goals

Proof state:
case a.h.mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t

Tactic:
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩

Result:
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_X_pow_le {R : Type*} [Semiring R] (n : ℕ) : (X ^ n : R[X]).natDegree ≤ n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).natDegree ≤ n

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a✝ : Nontrivial R
⊢ (X ^ n).natDegree ≤ n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a✝ : Nontrivial R
⊢ (X ^ n).natDegree ≤ n

Tactic:
rw [Polynomial.natDegree_X_pow]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_inv_inv_hom_hom_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom =
    f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv

Tactic:
simp

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Tactic:
rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]

Result:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x

Proof state:
case cons
x : Nat
xs : List Nat
ih : 0 < xs.sum ↔ ∃ x, x ∈ xs ∧ 0 < x
⊢ 0 < (x :: xs).sum ↔ ∃ x_1, x_1 ∈ x :: xs ∧ 0 < x_1

Tactic:
simp [← ih]

Result:
case cons
x : Nat
xs : List Nat
ih : 0 < xs.sum ↔ ∃ x, x ∈ xs ∧ 0 < x
⊢ 0 < x + xs.sum ↔ 0 < x ∨ 0 < xs.sum

Proof state:
case nil

⊢ 0 < [].sum ↔ ∃ x, x ∈ [] ∧ 0 < x

Tactic:
simp

Result:
no goals

Proof state:
l : List Nat
⊢ 0 < l.sum ↔ ∃ x, x ∈ l ∧ 0 < x

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp [← ih]
  omega

Result:
no goals

Proof state:
case cons
x : Nat
xs : List Nat
ih : 0 < xs.sum ↔ ∃ x, x ∈ xs ∧ 0 < x
⊢ 0 < x + xs.sum ↔ 0 < x ∨ 0 < xs.sum

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
lemma ShortExact.surjective_g [HasZeroObject C] (hS : S.ShortExact) :
    Function.Surjective ((forget₂ C Ab).map S.g)

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Epi S.g

Tactic:
exact hS.epi_g

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.g))

Tactic:
rw [← Preadditive.epi_iff_surjective]

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Epi S.g