harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : Array α) (h : ∀ b ∈ l.push a, P b) :
    pmap f (l.push a) h =
      (pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp)))

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
a : α
l : Array α
h : ∀ (b : α), b ∈ l.push a → P b
⊢ pmap f (l.push a) h = (pmap f l ⋯).push (f a ⋯)

Tactic:
simp [pmap]

Result:
no goals

Proof state:
α : Type ?u.5381
β : Type ?u.5424
P : α → Prop
f : (a : α) → P a → β
a : α
l : Array α
h : ∀ (b : α), b ∈ l.push a → P b
⊢ a ∈ l.push a

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.5381
β : Type ?u.5424
P : α → Prop
f : (a : α) → P a → β
a✝ : α
l : Array α
a : α
m : a ∈ l
h : ∀ (b : α), b ∈ l ∨ b = a✝ → P b
⊢ P a

Tactic:
exact h a (.inl m)

Result:
no goals

Proof state:
α : Type ?u.5381
β : Type ?u.5424
P : α → Prop
f : (a : α) → P a → β
a✝ : α
l : Array α
h : ∀ (b : α), b ∈ l.push a✝ → P b
a : α
m : a ∈ l
⊢ P a

Tactic:
simp at h

Result:
α : Type ?u.5381
β : Type ?u.5424
P : α → Prop
f : (a : α) → P a → β
a✝ : α
l : Array α
a : α
m : a ∈ l
h : ∀ (b : α), b ∈ l ∨ b = a✝ → P b
⊢ P a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem false_eq_true : (false = true) = False

Proof state:
⊢ (false = true) = False

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Induced.lean
@[simp]
lemma shiftFunctorZero_inv_app_obj_of_induced (X : C) :
    letI := HasShift.induced F A s i
    (shiftFunctorZero D A).inv.app (F.obj X) =
      F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_inv_app_obj]

Result:
no goals

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
⊢ (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
letI := HasShift.induced F A s i

Result:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_3, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X
-- Mathlib/MeasureTheory/SetAlgebra.lean
theorem generateSetAlgebra_subset {ℬ : Set (Set α)} (h : 𝒜 ⊆ ℬ)
    (hℬ : IsSetAlgebra ℬ) : generateSetAlgebra 𝒜 ⊆ ℬ

Proof state:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
⊢ generateSetAlgebra 𝒜 ⊆ ℬ

Tactic:
intro s hs

Result:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ ℬ

Proof state:
case empty
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
⊢ ∅ ∈ ℬ

Tactic:
exact hℬ.empty_mem

Result:
no goals

Proof state:
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s : Set α
hs : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ ℬ

Tactic:
induction hs with
| base t t_mem => exact h t_mem
| empty => exact hℬ.empty_mem
| compl t _ t_mem => exact hℬ.compl_mem t_mem
| union t u _ _ t_mem u_mem => exact hℬ.union_mem t_mem u_mem

Result:
no goals

Proof state:
case compl
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
hs✝ : generateSetAlgebra 𝒜 t
t_mem : t ∈ ℬ
⊢ tᶜ ∈ ℬ

Tactic:
exact hℬ.compl_mem t_mem

Result:
no goals

Proof state:
case base
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ ℬ

Tactic:
exact h t_mem

Result:
no goals

Proof state:
case union
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t u : Set α
hs✝ : generateSetAlgebra 𝒜 t
ht✝ : generateSetAlgebra 𝒜 u
t_mem : t ∈ ℬ
u_mem : u ∈ ℬ
⊢ t ∪ u ∈ ℬ

Tactic:
exact hℬ.union_mem t_mem u_mem

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem IsIntegral.mem_of_inv_mem (int : IsIntegral R x) (inv_mem : x⁻¹ ∈ A) : x ∈ A

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x⁻¹⁻¹ ∈ A

Tactic:
exact int.inv.inv_mem inv_mem

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x ∈ A

Tactic:
rw [← inv_inv x]

Result:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x⁻¹⁻¹ ∈ A
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_isSome_iff {f : α → Option β} {l : Vector α n} :
    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
l : Vector α n
⊢ (findSome? f l).isSome = true ↔ ∃ x, x ∈ l ∧ (f x).isSome = true

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true ↔
    ∃ x, x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ (f x).isSome = true

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true ↔
    ∃ x, x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ (f x).isSome = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma not_boundaryGE_next' [e.IsRelIff] {j k : ι} (hj : ¬ e.BoundaryGE j) (hk : c.next j = k) :
    ¬ e.BoundaryGE k

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
subst hk

Result:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hjk : ¬c.Rel j (c.next j)
⊢ ¬e.BoundaryGE (c.next j)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
⊢ ¬e.BoundaryGE k

Tactic:
by_cases hjk : c.Rel j k

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : c.Rel j k
⊢ ¬e.BoundaryGE k

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
exact e.not_boundaryGE_next hjk

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hjk : ¬c.Rel j (c.next j)
⊢ ¬e.BoundaryGE (c.next j)

Tactic:
simpa only [c.next_eq_self j hjk] using hj

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forIn_toList [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn as.toList b f = forIn as b f

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b : β
f : α → β → m (ForInStep β)
toList✝ : List α
⊢ forIn { toList := toList✝ }.toList b f = forIn { toList := toList✝ } b f

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as : Array α
b : β
f : α → β → m (ForInStep β)
⊢ forIn as.toList b f = forIn as b f

Tactic:
cases as

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b : β
f : α → β → m (ForInStep β)
toList✝ : List α
⊢ forIn { toList := toList✝ }.toList b f = forIn { toList := toList✝ } b f
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalComp_nil_nil {f g h i : C} (α : f ≅ g) (β : h ≅ i) :
    (α ⊗ β).hom = (α ⊗ β).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
α : f ≅ g
β : h ≅ i
⊢ (α ⊗ β).hom = (α ⊗ β).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_assoc {γ : Type*} {u : Finset γ}
    {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε}
    {g' : β → γ → ε'} (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) :
    image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u) :=
  coe_injective <| by
    push_cast
    exact image2_assoc h_assoc

Proof state:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst✝² : DecidableEq ε
inst✝¹ : DecidableEq ε'
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ ↑(image₂ f (image₂ g s t) u) = ↑(image₂ f' s (image₂ g' t u))

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst✝² : DecidableEq ε
inst✝¹ : DecidableEq ε'
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u = image2 f' (↑s) (image2 g' ↑t ↑u)

Proof state:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst✝² : DecidableEq ε
inst✝¹ : DecidableEq ε'
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u = image2 f' (↑s) (image2 g' ↑t ↑u)

Tactic:
exact image2_assoc h_assoc

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_div_of_mul_eq'' (h : c * a = b) : a = b / c

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : c * a = b
⊢ a = b / c

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma containsIdentities (hP : RingHom.ContainsIdentities Q) : P.ContainsIdentities where
  id_mem X

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
⊢ ∀ (i : ↑X.affineOpens), P (𝟙 X ∣_ ↑i)

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : ↑X.affineOpens
⊢ P (𝟙 X ∣_ ↑U)

Tactic:
have : IsAffine (𝟙 X ⁻¹ᵁ U.1) := U.2

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ P (𝟙 X ∣_ ↑U)

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (𝟙 Γ(↑(𝟙 X ⁻¹ᵁ ↑U), ⊤)))

Tactic:
apply hP

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
⊢ ∀ (i : ↑X.affineOpens), P (𝟙 X ∣_ ↑i)

Tactic:
intro U

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : ↑X.affineOpens
⊢ P (𝟙 X ∣_ ↑U)

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ P (𝟙 X ∣_ ↑U)

Tactic:
rw [morphismRestrict_id, iff_of_isAffine (P := P), Scheme.id_appTop]

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (𝟙 Γ(↑(𝟙 X ⁻¹ᵁ ↑U), ⊤)))
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
lemma AffineIndependent.card_le_finrank_succ [Fintype ι] {p : ι → P} (hp : AffineIndependent k p) :
    Fintype.card ι ≤ Module.finrank k (vectorSpan k (Set.range p)) + 1

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
⊢ Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
h✝ : IsEmpty ι
⊢ Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1

case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
h✝ : Nonempty ι
⊢ Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1

Proof state:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
h✝ : Nonempty ι
⊢ Fintype.card ι - 1 ≤ finrank k ↥(vectorSpan k (Set.range p))

Tactic:
exact (affineIndependent_iff_le_finrank_vectorSpan _ _
  (tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1 hp

Result:
no goals

Proof state:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
h✝ : IsEmpty ι
⊢ Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
simp [Fintype.card_eq_zero]

Result:
no goals

Proof state:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
h✝ : Nonempty ι
⊢ Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
rw [← tsub_le_iff_right]

Result:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
h✝ : Nonempty ι
⊢ Fintype.card ι - 1 ≤ finrank k ↥(vectorSpan k (Set.range p))
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Ici : (fun x => x - a) ⁻¹' Ici b = Ici (b + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) ⁻¹' Ici b = Ici (b + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
lemma equalizerConditionMap_iff_nonempty_isLimit (P : Cᵒᵖ ⥤ D) ⦃X B : C⦄ (π : X ⟶ B)
    [HasPullback π π] : SingleEqualizerCondition P π ↔
      Nonempty (IsLimit (P.mapCone
        (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows.cocone.op))

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
h : IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op)
⊢ SingleEqualizerCondition P π

Tactic:
exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ SingleEqualizerCondition P π ↔
    Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ SingleEqualizerCondition P π →
    Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))

case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op)) →
    SingleEqualizerCondition P π

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ SingleEqualizerCondition P π →
    Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))

Tactic:
intro h

Result:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
h : SingleEqualizerCondition P π
⊢ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
h : SingleEqualizerCondition P π
⊢ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))

Tactic:
exact ⟨isLimit_forkOfι_equiv _ _ _ (pullbackIsPullback π π) (h _ (pullbackIsPullback π π)).some⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op)) →
    SingleEqualizerCondition P π

Tactic:
intro ⟨h⟩

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
h : IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op)
⊢ SingleEqualizerCondition P π
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem ker_coe_equiv (f : R ≃+* S) : ker (f : R →+* S) = ⊥

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
x✝ : R
⊢ x✝ ∈ ker ↑f ↔ x✝ ∈ ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
⊢ ker ↑f = ⊥

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
x✝ : R
⊢ x✝ ∈ ker ↑f ↔ x✝ ∈ ⊥
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
/-- The angle ∠ABB at a point is always `π / 2`. -/
@[simp] lemma angle_self_right (p₀ p : P) : ∠ p p₀ p₀ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ ∠ p p₀ p₀ = π / 2

Tactic:
rw [angle_comm, angle_self_left]

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

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

Tactic:
subst m

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

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 : Nat
f : (i : Nat) → i < n → Bool
⊢ n.any f = n.any fun i h => f i ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem beq_ext {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
    (h : ∀ x y, @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) :
    inst1 = inst2

Proof state:
case e_beq.h.h
α : Type u_1
inst1 inst2 : BEq α
beq1 beq2 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
x y : α
⊢ beq1 x y = beq2 x y

Tactic:
exact h x y

Result:
no goals

Proof state:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 } = inst2

Tactic:
have ⟨beq2⟩ := inst2

Result:
α : Type u_1
inst1 inst2 : BEq α
beq1 beq2 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 } = { beq := beq2 }

Proof state:
case e_beq
α : Type u_1
inst1 inst2 : BEq α
beq1 beq2 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ beq1 = beq2

Tactic:
funext x y

Result:
case e_beq.h.h
α : Type u_1
inst1 inst2 : BEq α
beq1 beq2 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
x y : α
⊢ beq1 x y = beq2 x y

Proof state:
α : Type u_1
inst1 inst2 : BEq α
beq1 beq2 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 } = { beq := beq2 }

Tactic:
congr

Result:
case e_beq
α : Type u_1
inst1 inst2 : BEq α
beq1 beq2 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ beq1 = beq2

Proof state:
α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2

Tactic:
have ⟨beq1⟩ := inst1

Result:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 } = inst2