harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem lift_rank_mul_lift_rank :
    Cardinal.lift.{w} (Module.rank F K) * Cardinal.lift.{v} (Module.rank K A) =
      Cardinal.lift.{v} (Module.rank F A)

Proof state:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
  ← lift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
  lift_lift, lift_lift, lift_umax.{v, w}]

Result:
no goals

Proof state:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
let c := Module.Free.chooseBasis K A

Result:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Proof state:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
let b := Module.Free.chooseBasis F K

Result:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
-- Mathlib/Data/Fin/Basic.lean
theorem coe_of_injective_castLE_symm {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi) :
    ((Equiv.ofInjective _ (castLE_injective h)).symm ⟨i, hi⟩ : ℕ) = i

Proof state:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
rw [← coe_castLE h]

Result:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑(castLE h ((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩)) = ↑i

Proof state:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑(castLE h ((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩)) = ↑i

Tactic:
exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp] lemma map₂_coe_right (f : α → β → γ) (a) (b : β) : map₂ f a b = a.map (f · b)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithTop α
b : β
⊢ map₂ f a ↑b = map (fun x => f x b) a

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_of_xn_modEq_lem2 {n} (h : 2 * xn a1 n = xn a1 (n + 1)) : a = 2 ∧ n = 0

Proof state:
case refl
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ 0 = 0

Tactic:
exact ⟨h.symm, rfl⟩

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
this : n = 0
⊢ a = 2 ∧ n = 0

Tactic:
cases this

Result:
case refl
a : ℕ
a1 : 1 < a
h : xn a1 0 * 2 = xn a1 0 * a + Pell.d a1 * yn a1 0
⊢ a = 2 ∧ 0 = 0

Proof state:
case refl
a : ℕ
a1 : 1 < a
h : xn a1 0 * 2 = xn a1 0 * a + Pell.d a1 * yn a1 0
⊢ a = 2 ∧ 0 = 0

Tactic:
simp at h

Result:
case refl
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ 0 = 0

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
⊢ a = 2 ∧ n = 0

Tactic:
have : n = 0 :=
  n.eq_zero_or_pos.resolve_right fun np =>
    _root_.ne_of_lt
      (lt_of_le_of_lt (Nat.mul_le_mul_left _ a1)
        (Nat.lt_add_of_pos_right <| mul_pos (d_pos a1) (strictMono_y a1 np)))
      h

Result:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
this : n = 0
⊢ a = 2 ∧ n = 0

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
h : 2 * xn a1 n = xn a1 (n + 1)
⊢ a = 2 ∧ n = 0

Tactic:
rw [xn_succ, mul_comm] at h

Result:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
⊢ a = 2 ∧ n = 0
-- Mathlib/Tactic/ComputeDegree.lean
theorem coeff_sub_of_eq {n : ℕ} {a b : R} {f g : R[X]} (hf : f.coeff n = a) (hg : g.coeff n = b) :
    (f - g).coeff n = a - b

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : R
f g : R[X]
hf : f.coeff n = a
hg : g.coeff n = b
⊢ (f - g).coeff n = a - b

Tactic:
subst hf hg

Result:
R : Type u_1
inst✝ : Ring R
n : ℕ
f g : R[X]
⊢ (f - g).coeff n = f.coeff n - g.coeff n

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
f g : R[X]
⊢ (f - g).coeff n = f.coeff n - g.coeff n

Tactic:
apply coeff_sub

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem pullbackZeroZeroIso_hom_snd (X Y : C) [HasBinaryProduct X Y] :
    (pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd 0 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd 0 0

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem mul_adjp_add_detp : A * adjp 1 A + detp (-1) A • 1 = A * adjp (-1) A + detp 1 A • 1

Proof state:
case a
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
⊢ (A * adjp 1 A + detp (-1) A • 1) i j = (A * adjp (-1) A + detp 1 A • 1) i j

Tactic:
rcases eq_or_ne i j with rfl | h <;> simp_rw [add_apply, smul_apply, smul_eq_mul]

Result:
case a.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i : n
⊢ (A * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i

case a.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
⊢ (A * adjp 1 A) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j

Proof state:
case a.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
⊢ (A * adjp 1 A) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j

Tactic:
simp_rw [mul_adjp_apply_ne A i j h, one_apply_ne h, mul_zero]

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
⊢ A * adjp 1 A + detp (-1) A • 1 = A * adjp (-1) A + detp 1 A • 1

Tactic:
ext i j

Result:
case a
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
⊢ (A * adjp 1 A + detp (-1) A • 1) i j = (A * adjp (-1) A + detp 1 A • 1) i j

Proof state:
case a.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i : n
⊢ (A * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i

Tactic:
simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ici_add_one_eq_Ioi_of_not_isMax (ha : ¬ IsMax a) : Ici (a + 1) = Ioi a

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi_of_not_isMax ha

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma predAbove_right_zero [NeZero n] {i : Fin n} : predAbove (i : Fin n) 0 = 0

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ i.predAbove 0 = 0

Tactic:
rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.predAbove 0 = 0

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
i : Fin 0
⊢ i.predAbove 0 = 0

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ i.predAbove 0 = 0

Proof state:
case zero
inst✝ : NeZero 0
i : Fin 0
⊢ i.predAbove 0 = 0

Tactic:
exact i.elim0

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.desc_inl_inr {X Y : C} [HasBinaryCoproduct X Y] :
    coprod.desc coprod.inl coprod.inr = 𝟙 (X ⨿ Y)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ desc inl inr = 𝟙 (X ⨿ Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem isBounded_iff_nndist {s : Set α} :
    IsBounded s ↔ ∃ C : ℝ≥0, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → nndist x y ≤ C

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C

Tactic:
simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
  NNReal.coe_mk, exists_prop]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem TransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
    (h : ∀ a b, r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) :
    TransGen p (f a) (f b)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → TransGen p (f a) (f b)
hab : TransGen r a b
⊢ TransGen p (f a) (f b)

Tactic:
simpa [transGen_idem] using hab.lift f h

Result:
no goals
-- Mathlib/Data/Part.lean
theorem append_get_eq [Append α] (a b : Part α) (hab : Dom (a ++ b)) : (a ++ b).get hab =
    a.get (left_dom_of_append_dom hab) ++ b.get (right_dom_of_append_dom hab)

Proof state:
α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a.bind fun y => map (fun x => y ++ x) b).get ⋯ = a.get ⋯ ++ b.get ⋯

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a ++ b).get hab = a.get ⋯ ++ b.get ⋯

Tactic:
simp [append_def]

Result:
α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a.bind fun y => map (fun x => y ++ x) b).get ⋯ = a.get ⋯ ++ b.get ⋯
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
an arrow `i` with `i + 1 > j` can be identified with arrow `i + 1` in the
original path. -/
lemma spine_δ_arrow_gt (f : Path X (n + 1)) {i : Fin n} {j : Fin (n + 2)}
    (h : j < i.succ.castSucc) :
    (X.spine n (X.δ j (spineToSimplex f))).arrow i = f.arrow i.succ

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ X.map (mkOfSucc i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.arrow i.succ

Tactic:
rw [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ X.map (mkOfSucc i ≫ SimplexCategory.δ j).op (spineToSimplex f) = f.arrow i.succ

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (X.spine n (SimplicialObject.δ X j (spineToSimplex f))).arrow i = f.arrow i.succ

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ X.map (mkOfSucc i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.arrow i.succ

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ X.map (mkOfSucc i ≫ SimplexCategory.δ j).op (spineToSimplex f) = f.arrow i.succ

Tactic:
rw [mkOfSucc_δ_gt h, spineToSimplex_arrow]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_single_same (i : ι) (x : β i) : (single i x).erase i = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
x : β i
⊢ erase i (single i x) = 0

Tactic:
rw [erase_single, if_pos rfl]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtomistic_dual_iff_isCoatomistic : IsAtomistic αᵒᵈ ↔ IsCoatomistic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_sSup_atoms⟩, fun h => ⟨fun b => by apply h.eq_sInf_coatoms⟩⟩

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsCoatomistic α
b : αᵒᵈ
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
apply h.eq_sInf_coatoms

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsAtomistic αᵒᵈ
b : α
⊢ ∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a

Tactic:
apply h.eq_sSup_atoms

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
    l.foldr (fun k v acc => f k v :: acc) acc =
      (l.toList.map (fun p => f p.1 p.2)) ++ acc

Proof state:
α : Type u
β : α → Type v
δ : Type w
l : AssocList α β
acc : List δ
f : (a : α) → β a → δ
⊢ foldr (fun k v acc => f k v :: acc) acc l = List.map (fun p => f p.fst p.snd) l.toList ++ acc

Tactic:
induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem diff_nonempty_of_ncard_lt_ncard (h : s.ncard < t.ncard) (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : autoParam s.Finite _auto✝
⊢ (t \ s).Nonempty

Tactic:
rw [Set.nonempty_iff_ne_empty, Ne, diff_eq_empty]

Result:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : autoParam s.Finite _auto✝
⊢ ¬t ⊆ s

Proof state:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : autoParam s.Finite _auto✝
⊢ ¬t ⊆ s

Tactic:
exact fun h' ↦ h.not_le (ncard_le_ncard h' hs)

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem map_univ_coeEmbedding (m : Multiset α) :
    (Finset.univ : Finset m).map m.coeEmbedding = m.toEnumFinset

Proof state:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map m.coeEmbedding Finset.univ ↔ (x, i) ∈ m.toEnumFinset

Tactic:
simp only [Fin.exists_iff, Finset.mem_map, Finset.mem_univ, Multiset.coeEmbedding_apply,
  Prod.mk.inj_iff, exists_true_left, Multiset.exists_coe, Multiset.coe_mk, Fin.val_mk,
  exists_prop, exists_eq_right_right, exists_eq_right, Multiset.mem_toEnumFinset, true_and]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset

Tactic:
ext ⟨x, i⟩

Result:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ Finset.map m.coeEmbedding Finset.univ ↔ (x, i) ∈ m.toEnumFinset
-- Mathlib/CategoryTheory/Sites/Types.lean
theorem eval_typesGlue {S hs α} (f) : eval.{u} S α (typesGlue S hs α f) = f

Proof state:
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : α
⊢ eval S α (typesGlue S hs α f) x = f x

Tactic:
apply (IsSheafFor.valid_glue _ _ _ <| ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩).trans

Result:
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : α
⊢ S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose ⋯))) = f x

Proof state:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
⊢ eval S α (typesGlue S hs α f) = f

Tactic:
funext x

Result:
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : α
⊢ eval S α (typesGlue S hs α f) x = f x

Proof state:
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : α
⊢ S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose ⋯))) = f x

Tactic:
convert FunctorToTypes.map_id_apply S _

Result:
no goals
-- Mathlib/Algebra/Lie/CartanExists.lean
lemma exists_isCartanSubalgebra_engel [Infinite K] :
    ∃ x : L, IsCartanSubalgebra (engel K x)

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : Module.Finite K L
inst✝ : Infinite K
⊢ ↑(finrank K L) ≤ #K

Tactic:
exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite K›

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : Module.Finite K L
inst✝ : Infinite K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
apply exists_isCartanSubalgebra_engel_of_finrank_le_card

Result:
case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : Module.Finite K L
inst✝ : Infinite K
⊢ ↑(finrank K L) ≤ #K
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem findSome?_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findSome? f = l.unattach.findSome? g

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Array.findSome? f l = Array.findSome? g l.unattach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk.nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Array.findSome? f { toList := [] } = Array.findSome? g { toList := [] }.unattach

case mk.cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Array.findSome? f { toList := head✝ :: tail✝ } = Array.findSome? g { toList := head✝ :: tail✝ }.unattach

Proof state:
case mk.cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Array.findSome? f { toList := head✝ :: tail✝ } = Array.findSome? g { toList := head✝ :: tail✝ }.unattach

Tactic:
rw [Array.findSome?_subtype hf]

Result:
no goals

Proof state:
case mk.nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Array.findSome? f { toList := [] } = Array.findSome? g { toList := [] }.unattach

case mk.cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Array.findSome? f { toList := head✝ :: tail✝ } = Array.findSome? g { toList := head✝ :: tail✝ }.unattach

Tactic:
simp

Result:
case mk.cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Array.findSome? f { toList := head✝ :: tail✝ } = Array.findSome? g { toList := head✝ :: tail✝ }.unattach
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin (h : IsSymmSndFDerivWithinAt 𝕜 f t x)
    (hst : t ∈ 𝓝[s] x) (hf : ContDiffWithinAt 𝕜 2 f t x)
    (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hx : x ∈ s) :
    IsSymmSndFDerivWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) w) v

Tactic:
exact h v w

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v

Tactic:
rw [fderivWithin_fderivWithin_eq_of_mem_nhdsWithin hst hf hs ht hx]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) w) v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
intro v w

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem orderTop_one [MulZeroOneClass R] [Nontrivial R] : orderTop (1 : HahnSeries Γ R) = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝³ : Zero Γ
inst✝² : PartialOrder Γ
inst✝¹ : MulZeroOneClass R
inst✝ : Nontrivial R
⊢ orderTop 1 = 0

Tactic:
rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem Ring.inverse_star [Semiring R] [StarRing R] (a : R) :
    Ring.inverse (star a) = star (Ring.inverse a)

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ inverse (star a) = star (inverse a)

Tactic:
rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
⊢ inverse (star a) = star (inverse a)

Tactic:
by_cases ha : IsUnit a

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ inverse (star a) = star (inverse a)

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ inverse (star a) = star (inverse a)

Proof state:
case pos.intro
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ inverse (star ↑u) = star (inverse ↑u)

Tactic:
rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ inverse (star a) = star (inverse a)

Tactic:
obtain ⟨u, rfl⟩ := ha

Result:
case pos.intro
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ inverse (star ↑u) = star (inverse ↑u)