harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Adhesive.lean
theorem adhesive_of_preserves_and_reflects (F : C ⥤ D) [Adhesive D]
    [H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g]
    [H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g]
    [PreservesLimitsOfShape WalkingCospan F]
    [ReflectsLimitsOfShape WalkingCospan F]
    [PreservesColimitsOfShape WalkingSpan F]
    [ReflectsColimitsOfShape WalkingSpan F] :
    Adhesive C

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    ((Cocones.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))

Tactic:
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ ⋯.IsVanKampen

Tactic:
apply Adhesive.van_kampen

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem back?_filter (p : α → Bool) (l : Array α) : (l.filter p).back? = l.findRev? p

Proof state:
α : Type
p : α → Bool
l : Array α
⊢ (filter p l).back? = findRev? p l

Tactic:
cases l

Result:
case mk
α : Type
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ }).back? = findRev? p { toList := toList✝ }

Proof state:
case mk
α : Type
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ }).back? = findRev? p { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_negDblY (P : Fin 3 → R) : (W'.map f).toJacobian.negDblY (f ∘ P) = f (W'.negDblY P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.dblU P) * (f (W'.dblX P) - (⇑f ∘ P) x * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2) +
      (⇑f ∘ P) y * ((⇑f ∘ P) y - f (W'.negY P)) ^ 3 =
    f (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.negDblY (⇑f ∘ P) = f (W'.negDblY P)

Tactic:
simp only [negDblY, map_dblU, map_dblX, map_negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.dblU P) * (f (W'.dblX P) - (⇑f ∘ P) x * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2) +
      (⇑f ∘ P) y * ((⇑f ∘ P) y - f (W'.negY P)) ^ 3 =
    f (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem Filter.EventuallyEq.div_mul_cancel {α G : Type*} [GroupWithZero G] {f g : α → G}
    {l : Filter α} (hg : Tendsto g l (𝓟 {0}ᶜ)) : (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x

Proof state:
case h
α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
hx : x ∈ g ⁻¹' {0}ᶜ
⊢ f x / g x * g x = f x

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
⊢ (fun x => f x / g x * g x) =ᶠ[l] fun x => f x

Tactic:
filter_upwards [hg.le_comap <| preimage_mem_comap (m := g) (mem_principal_self {0}ᶜ)] with x hx

Result:
case h
α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
hx : x ∈ g ⁻¹' {0}ᶜ
⊢ f x / g x * g x = f x
-- Mathlib/Algebra/Homology/Embedding/TruncLE.lean
/-- `(K.truncLE'ToRestriction e).f i` is an isomorphism when `¬ e.BoundaryLE i`. -/
lemma isIso_truncLE'ToRestriction (i : ι) (hi : ¬ e.BoundaryLE i) :
    IsIso ((K.truncLE'ToRestriction e).f i)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop

Tactic:
have := K.op.isIso_restrictionToTruncGE' e.op i (by simpa)

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
this : IsIso ((K.op.restrictionToTruncGE' e.op).f i)
⊢ IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ IsIso ((K.truncLE'ToRestriction e).f i)

Tactic:
change IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
this : IsIso ((K.op.restrictionToTruncGE' e.op).f i)
⊢ IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop

Tactic:
infer_instance

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_succ_right (n : ℕ) :
    descPochhammer R (n + 1) = descPochhammer R n * (X - (n : R[X]))

Proof state:
case succ
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
⊢ descPochhammer ℤ (n + 1) * (X - 1 - ↑n) = descPochhammer ℤ (n + 1) * (X - ↑(n + 1))

Tactic:
rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
h : map (algebraMap ℤ R) (descPochhammer ℤ (n + 1)) = map (algebraMap ℤ R) (descPochhammer ℤ n * (X - ↑n))
⊢ descPochhammer R (n + 1) = descPochhammer R n * (X - ↑n)

Tactic:
simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
  Polynomial.map_intCast] using h

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ descPochhammer R (n + 1) = descPochhammer R n * (X - ↑n)

Tactic:
suffices h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - (n : ℤ[X])) by
  apply_fun Polynomial.map (algebraMap ℤ R) at h
  simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
    Polynomial.map_intCast] using h

Result:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
⊢ descPochhammer R (n + 1) = descPochhammer R n * (X - ↑n)

Tactic:
apply_fun Polynomial.map (algebraMap ℤ R) at h

Result:
R : Type u
inst✝ : Ring R
n : ℕ
h : map (algebraMap ℤ R) (descPochhammer ℤ (n + 1)) = map (algebraMap ℤ R) (descPochhammer ℤ n * (X - ↑n))
⊢ descPochhammer R (n + 1) = descPochhammer R n * (X - ↑n)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)

Tactic:
induction n with
| zero => simp [descPochhammer]
| succ n ih =>
  conv_lhs =>
    rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
        X_comp, natCast_comp]
  rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
⊢ descPochhammer ℤ (n + 1 + 1) = descPochhammer ℤ (n + 1) * (X - ↑(n + 1))

Tactic:
conv_lhs =>
  rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
      X_comp, natCast_comp]

Result:
case succ
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
⊢ descPochhammer ℤ (n + 1) * (X - 1 - ↑n) = descPochhammer ℤ (n + 1) * (X - ↑(n + 1))

Proof state:
case zero
R : Type u
inst✝ : Ring R
⊢ descPochhammer ℤ (0 + 1) = descPochhammer ℤ 0 * (X - ↑0)

Tactic:
simp [descPochhammer]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) : (m.alter k f).getKey! k' =
      if k == k' then
        if (f (m.get? k)).isSome then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getKey! k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'

Tactic:
simp_to_raw using Raw₀.getKey!_alter

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem map_bot [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) :
    (⊥ : NonUnitalStarSubalgebra R A).map f = ⊥ :=
  SetLike.coe_injective <| by simp [NonUnitalAlgebra.coe_bot, NonUnitalStarSubalgebra.coe_map]

Proof state:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : NonUnitalSemiring A
inst✝¹³ : StarRing A
inst✝¹² : Module R A
inst✝¹¹ : NonUnitalSemiring B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module R B
inst✝⁸ : FunLike F A B
inst✝⁷ : NonUnitalAlgHomClass F R A B
inst✝⁶ : StarHomClass F A B
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
⊢ ↑(map f ⊥) = ↑⊥

Tactic:
simp [NonUnitalAlgebra.coe_bot, NonUnitalStarSubalgebra.coe_map]

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem PNat.isUnit_natCast [h : Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))]
    (n : ℕ+) : IsUnit (n : R)

Proof state:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n ∈ Ideal.span {↑↑n}

Tactic:
exact Ideal.subset_span (Set.mem_singleton _)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ False

Tactic:
apply h_char_zero.cast_injective.ne n.ne_zero

Result:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n = ↑0

Proof state:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ IsUnit ↑↑n

Tactic:
rw [← Ideal.span_singleton_eq_top]

Result:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ Ideal.span {↑↑n} = ⊤

Proof state:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ Ideal.span {↑↑n} = ⊤

Tactic:
apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))

Result:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ¬CharZero (R ⧸ Ideal.span {↑↑n})

Proof state:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ¬CharZero (R ⧸ Ideal.span {↑↑n})

Tactic:
intro h_char_zero

Result:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n = ↑0

Tactic:
rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]

Result:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n ∈ Ideal.span {↑↑n}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_le_of_le_of_le {a b c : Nat} : a ≤ c → b ≤ c → max a b ≤ c

Proof state:
case inl
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
h : a ≤ b
⊢ max a b ≤ c

Tactic:
rw [Nat.max_eq_right h]

Result:
case inl
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
h : a ≤ b
⊢ b ≤ c

Proof state:
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
⊢ max a b ≤ c

Tactic:
cases Nat.le_total a b with
| inl h => rw [Nat.max_eq_right h]; assumption
| inr h => rw [Nat.max_eq_left h]; assumption

Result:
no goals

Proof state:
case inl
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
h : a ≤ b
⊢ b ≤ c

Tactic:
assumption

Result:
no goals

Proof state:
a b c : Nat
⊢ a ≤ c → b ≤ c → max a b ≤ c

Tactic:
intros

Result:
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
⊢ max a b ≤ c

Proof state:
case inr
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
h : b ≤ a
⊢ max a b ≤ c

Tactic:
rw [Nat.max_eq_left h]

Result:
case inr
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
h : b ≤ a
⊢ a ≤ c

Proof state:
case inr
a b c : Nat
a✝¹ : a ≤ c
a✝ : b ≤ c
h : b ≤ a
⊢ a ≤ c

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem results_think {s : Computation α} {a n} (h : Results s a n) : Results (think s) a (n + 1) :=
  haveI := h.terminates
  ⟨think_mem h.mem, by rw [length_think, h.length]⟩

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
⊢ s.think.length = n + 1

Tactic:
rw [length_think, h.length]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem eq_iInf_principal (B : FilterBasis α) : B.filter = ⨅ s : B.sets, 𝓟 s

Proof state:
case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V

Tactic:
exact subset_inter_iff.mp W_sub

Result:
no goals

Proof state:
case mk.mk.intro.intro
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ ∃ z,
    (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨U, U_in⟩) ((fun s => 𝓟 ↑s) z) ∧
      (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨V, V_in⟩) ((fun s => 𝓟 ↑s) z)

Tactic:
use ⟨W, W_in⟩

Result:
case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨U, U_in⟩) ((fun s => 𝓟 ↑s) ⟨W, W_in⟩) ∧
    (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨V, V_in⟩) ((fun s => 𝓟 ↑s) ⟨W, W_in⟩)

Proof state:
case mk.mk
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
⊢ ∃ z,
    (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨U, U_in⟩) ((fun s => 𝓟 ↑s) z) ∧
      (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨V, V_in⟩) ((fun s => 𝓟 ↑s) z)

Tactic:
rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩

Result:
case mk.mk.intro.intro
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ ∃ z,
    (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨U, U_in⟩) ((fun s => 𝓟 ↑s) z) ∧
      (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨V, V_in⟩) ((fun s => 𝓟 ↑s) z)

Proof state:
α : Type u_1
B : FilterBasis α
this : Directed (fun x1 x2 => x1 ≥ x2) fun s => 𝓟 ↑s
⊢ B.filter = ⨅ s, 𝓟 ↑s

Tactic:
ext U

Result:
case h
α : Type u_1
B : FilterBasis α
this : Directed (fun x1 x2 => x1 ≥ x2) fun s => 𝓟 ↑s
U : Set α
⊢ U ∈ B.filter ↔ U ∈ ⨅ s, 𝓟 ↑s

Proof state:
case h
α : Type u_1
B : FilterBasis α
this : Directed (fun x1 x2 => x1 ≥ x2) fun s => 𝓟 ↑s
U : Set α
⊢ U ∈ B.filter ↔ U ∈ ⨅ s, 𝓟 ↑s

Tactic:
simp [mem_filter_iff, mem_iInf_of_directed this]

Result:
no goals

Proof state:
α : Type u_1
B : FilterBasis α
⊢ Directed (fun x1 x2 => x1 ≥ x2) fun s => 𝓟 ↑s

Tactic:
rintro ⟨U, U_in⟩ ⟨V, V_in⟩

Result:
case mk.mk
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
⊢ ∃ z,
    (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨U, U_in⟩) ((fun s => 𝓟 ↑s) z) ∧
      (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨V, V_in⟩) ((fun s => 𝓟 ↑s) z)

Proof state:
case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨U, U_in⟩) ((fun s => 𝓟 ↑s) ⟨W, W_in⟩) ∧
    (fun x1 x2 => x1 ≥ x2) ((fun s => 𝓟 ↑s) ⟨V, V_in⟩) ((fun s => 𝓟 ↑s) ⟨W, W_in⟩)

Tactic:
simp only [le_principal_iff, mem_principal, Subtype.coe_mk]

Result:
case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V
-- Mathlib/Order/MinMax.lean
theorem Monotone.map_max (hf : Monotone f) : f (max a b) = max (f a) (f b)

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
⊢ f (a ⊔ b) = f a ⊔ f b

Tactic:
rcases le_total a b with h | h <;> simp [h, hf h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_le (a b : Ordinal) : (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Proof state:
case inl.intro.inl.intro
n m : ℕ
⊢ (↑n ^ ↑m).card ≤ ℵ₀ ⊔ ((↑n).card ⊔ (↑m).card)

Tactic:
rw [← natCast_opow, card_nat]

Result:
case inl.intro.inl.intro
n m : ℕ
⊢ ↑(n ^ m) ≤ ℵ₀ ⊔ ((↑n).card ⊔ (↑m).card)

Proof state:
a b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ ℵ₀ ⊔ (a.card ⊔ b.card)

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_nat_or_omega0_le a

Result:
case inl.intro
b : Ordinal.{u_1}
n : ℕ
⊢ (↑n ^ b).card ≤ ℵ₀ ⊔ ((↑n).card ⊔ b.card)

case inr
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ ℵ₀ ⊔ (a.card ⊔ b.card)

Proof state:
case inl.intro.inr
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (↑n ^ b).card ≤ ℵ₀ ⊔ ((↑n).card ⊔ b.card)

Tactic:
exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

Result:
no goals

Proof state:
case inl.intro
b : Ordinal.{u_1}
n : ℕ
⊢ (↑n ^ b).card ≤ ℵ₀ ⊔ ((↑n).card ⊔ b.card)

Tactic:
obtain ⟨m, rfl⟩ | hb := eq_nat_or_omega0_le b

Result:
case inl.intro.inl.intro
n m : ℕ
⊢ (↑n ^ ↑m).card ≤ ℵ₀ ⊔ ((↑n).card ⊔ (↑m).card)

case inl.intro.inr
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (↑n ^ b).card ≤ ℵ₀ ⊔ ((↑n).card ⊔ b.card)

Proof state:
case inr
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ ℵ₀ ⊔ (a.card ⊔ b.card)

Tactic:
exact (card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

Result:
no goals

Proof state:
case inl.intro.inl.intro
n m : ℕ
⊢ ↑(n ^ m) ≤ ℵ₀ ⊔ ((↑n).card ⊔ (↑m).card)

Tactic:
exact le_max_of_le_left (nat_lt_aleph0 _).le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
    ¬a ∈ m → m.getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
a : α
fallback : β a
⊢ ¬a ∈ m → m.getD a fallback = fallback

Tactic:
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem getLeft_eq_getLeft? (h₁ : x.isLeft) (h₂ : x.getLeft?.isSome) :
    x.getLeft h₁ = x.getLeft?.get h₂

Proof state:
α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isLeft = true
h₂ : x.getLeft?.isSome = true
⊢ x.getLeft h₁ = x.getLeft?.get h₂

Tactic:
simp [← getLeft?_eq_some_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem face_centroid_eq_iff [CharZero k] {n : ℕ} (s : Simplex k P n)
    {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) :
    Finset.univ.centroid k (s.face h₁).points = Finset.univ.centroid k (s.face h₂).points ↔
      fs₁ = fs₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
⊢ centroid k fs₁ s.points = centroid k fs₂ s.points ↔ fs₁ = fs₂

Tactic:
exact s.centroid_eq_iff h₁ h₂

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
⊢ centroid k univ (s.face h₁).points = centroid k univ (s.face h₂).points ↔ fs₁ = fs₂

Tactic:
rw [face_centroid_eq_centroid, face_centroid_eq_centroid]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
⊢ centroid k fs₁ s.points = centroid k fs₂ s.points ↔ fs₁ = fs₂
-- Mathlib/Topology/Bases.lean
theorem isSeparable_union {s t : Set α} : IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t

Proof state:
α : Type u
t✝ : TopologicalSpace α
s t : Set α
⊢ IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t

Tactic:
simp [union_eq_iUnion, and_comm]

Result:
no goals