harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/CartanExists.lean
lemma lieCharpoly_natDegree [Nontrivial R] : (lieCharpoly R M x y).natDegree = finrank R M

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
⊢ (LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).natDegree = finrank R M

Tactic:
rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Lattice.lean
theorem coprod_eq_sup [SemilatticeSup α] [OrderBot α] (x y : α) : Limits.coprod x y = x ⊔ y :=
  calc
    Limits.coprod x y = colimit (pair x y) := rfl
    _ = Finset.univ.sup (pair x y).obj

Proof state:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ x ⊔ (y ⊔ ⊥) = x ⊔ y

Tactic:
rw [sup_bot_eq]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ colimit (pair x y) = Finset.univ.sup (pair x y).obj

Tactic:
rw [finite_colimit_eq_finset_univ_sup (pair x y)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_sub_left_le {a b c : Int} (h : a - b ≤ c) : a ≤ b + c

Proof state:
a b c : Int
h✝ : a - b ≤ c
h : a - b + b ≤ c + b
⊢ a ≤ b + c

Tactic:
rwa [Int.sub_add_cancel, Int.add_comm] at h

Result:
no goals

Proof state:
a b c : Int
h : a - b ≤ c
⊢ a ≤ b + c

Tactic:
have h := Int.add_le_add_right h b

Result:
a b c : Int
h✝ : a - b ≤ c
h : a - b + b ≤ c + b
⊢ a ≤ b + c
-- Mathlib/Data/PNat/Factors.lean
theorem prod_inf (u v : PrimeMultiset) : (u ⊓ v).prod = PNat.gcd u.prod v.prod

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Tactic:
let m := v.prod

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊓ v).prod = n.gcd m

Tactic:
rw [this]

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Tactic:
change (u ⊓ v).prod = PNat.gcd n m

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = n.gcd m

Proof state:
u v : PrimeMultiset
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Tactic:
let n := u.prod

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
⊢ (u ⊓ v).prod = u.prod.gcd v.prod

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = n.gcd m

Tactic:
have : u = n.factorMultiset := u.factorMultiset_prod.symm

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊓ v).prod = n.gcd m

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m

Tactic:
rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]

Result:
no goals

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m

Tactic:
have : v = m.factorMultiset := v.factorMultiset_prod.symm

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m

Tactic:
rw [this]

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ m.factorMultiset).prod = n.gcd m
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.inl_ofComponents :
    biprod.inl ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ biprod.inl ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr

Tactic:
simp [Biprod.ofComponents]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma natDegree_preHilbertPoly [CharZero F] (d k : ℕ) :
    (preHilbertPoly F d k).natDegree = d

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ (preHilbertPoly F d k).natDegree = d

Tactic:
rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
  add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, mul_one]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ¬d ! = 0

Tactic:
positivity

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).natDegree = d

Tactic:
have hne : (d ! : F) ≠ 0 := by norm_cast; positivity

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ (preHilbertPoly F d k).natDegree = d

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ↑d ! ≠ 0

Tactic:
norm_cast

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ¬d ! = 0
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem le_of_lt_minimalPeriod_of_iterate_eq {m n : ℕ} (hm : m < minimalPeriod f x)
    (hmn : f^[m] x = f^[n] x) : m ≤ n

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ False

Tactic:
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m ≤ n

Tactic:
by_contra! hmn'

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ False

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False

Tactic:
exact
  ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
            (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
              (minimalPeriod_pos_iff_mem_periodicPts.1 ((zero_le m).trans_lt hm)) hmn)).trans
        (Nat.sub_le m n)).not_lt
    hm

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean
@[simp]
lemma map_d (b : B) : map fac (d b) = d (g' b)

Proof state:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
have := IsScalarTower.of_algebraMap_eq' (congrArg Hom.hom fac)

Result:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
this : IsScalarTower ↑A ↑B ↑B'
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Proof state:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
algebraize [f.hom, f'.hom, g.hom, g'.hom, f'.hom.comp g.hom]

Result:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Proof state:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
this : IsScalarTower ↑A ↑B ↑B'
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
exact _root_.KaehlerDifferential.map_D A A' B B' b

Result:
no goals
-- Mathlib/Topology/Algebra/MulAction.lean
lemma IsScalarTower.continuousSMul {M : Type*} (N : Type*) {α : Type*} [Monoid N] [SMul M N]
    [MulAction N α] [SMul M α] [IsScalarTower M N α] [TopologicalSpace M] [TopologicalSpace N]
    [TopologicalSpace α] [ContinuousSMul M N] [ContinuousSMul N α] : ContinuousSMul M α :=
  { continuous_smul

Proof state:
M : Type u_5
N : Type u_6
α : Type u_7
inst✝⁹ : Monoid N
inst✝⁸ : SMul M N
inst✝⁷ : MulAction N α
inst✝⁶ : SMul M α
inst✝⁵ : IsScalarTower M N α
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousSMul M N
inst✝ : ContinuousSMul N α
⊢ Continuous fun p => (p.1 • 1) • p.2

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_5
N : Type u_6
α : Type u_7
inst✝⁹ : Monoid N
inst✝⁸ : SMul M N
inst✝⁷ : MulAction N α
inst✝⁶ : SMul M α
inst✝⁵ : IsScalarTower M N α
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousSMul M N
inst✝ : ContinuousSMul N α
this : Continuous fun p => (p.1 • 1) • p.2
⊢ Continuous fun p => p.1 • p.2

Tactic:
simpa

Result:
no goals

Proof state:
M : Type u_5
N : Type u_6
α : Type u_7
inst✝⁹ : Monoid N
inst✝⁸ : SMul M N
inst✝⁷ : MulAction N α
inst✝⁶ : SMul M α
inst✝⁵ : IsScalarTower M N α
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousSMul M N
inst✝ : ContinuousSMul N α
⊢ Continuous fun p => p.1 • p.2

Tactic:
suffices Continuous (fun p : M × α ↦ (p.1 • (1 : N)) • p.2) by simpa

Result:
M : Type u_5
N : Type u_6
α : Type u_7
inst✝⁹ : Monoid N
inst✝⁸ : SMul M N
inst✝⁷ : MulAction N α
inst✝⁶ : SMul M α
inst✝⁵ : IsScalarTower M N α
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousSMul M N
inst✝ : ContinuousSMul N α
⊢ Continuous fun p => (p.1 • 1) • p.2
-- Mathlib/Algebra/Homology/ConcreteCategory.lean
@[simp]
lemma i_cyclesMk {i : ι} (x : (forget₂ C Ab).obj (K.X i)) (j : ι) (hj : c.next i = j)
    (hx : ((forget₂ C Ab).map (K.d i j)) x = 0) :
    ((forget₂ C Ab).map (K.iCycles i)) (K.cyclesMk x j hj hx) = x

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
x : ↑((forget₂ C Ab).obj (K.X i))
hx : (ConcreteCategory.hom ((forget₂ C Ab).map (K.d i (c.next i)))) x = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (K.iCycles i))) (K.cyclesMk x (c.next i) ⋯ hx) = x

Tactic:
apply (K.sc i).i_cyclesMk

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
x : ↑((forget₂ C Ab).obj (K.X i))
j : ι
hj : c.next i = j
hx : (ConcreteCategory.hom ((forget₂ C Ab).map (K.d i j))) x = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (K.iCycles i))) (K.cyclesMk x j hj hx) = x

Tactic:
subst hj

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
x : ↑((forget₂ C Ab).obj (K.X i))
hx : (ConcreteCategory.hom ((forget₂ C Ab).map (K.d i (c.next i)))) x = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (K.iCycles i))) (K.cyclesMk x (c.next i) ⋯ hx) = x
-- Mathlib/Order/Atoms.lean
theorem isSimpleOrder_iff_isSimpleOrder_orderDual [LE α] [BoundedOrder α] :
    IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ

Proof state:
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ

Tactic:
constructor <;> intro i <;> haveI := i

Result:
case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ

case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Proof state:
case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
exact
  { exists_pair_ne := @exists_pair_ne αᵒᵈ _
    eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i this : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ

Tactic:
exact
  { exists_pair_ne := @exists_pair_ne α _
    eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Module.card_fintype [Fintype ι] (b : Basis ι R M) [Fintype R] [Fintype M] :
    card M = card R ^ card ι

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι

Tactic:
calc
  card M = card (ι → R) := card_congr b.equivFun.toEquiv
  _ = card R ^ card ι := card_fun

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι

Tactic:
classical
  calc
    card M = card (ι → R) := card_congr b.equivFun.toEquiv
    _ = card R ^ card ι := card_fun

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_zero_iff_subsingleton [IsNilpotent G] :
    Group.nilpotencyClass G = 0 ↔ Subsingleton G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
classical
rw [Group.nilpotencyClass, Nat.find_eq_zero, upperCentralSeries_zero,
  subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
rw [Group.nilpotencyClass, Nat.find_eq_zero, upperCentralSeries_zero,
  subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Schur.lean
theorem finrank_hom_simple_simple_eq_zero_of_not_iso [HasKernels C] [Linear 𝕜 C] {X Y : C}
    [Simple X] [Simple Y] (h : (X ≅ Y) → False) : finrank 𝕜 (X ⟶ Y) = 0 :=
  haveI :=
    subsingleton_of_forall_eq (0 : X ⟶ Y) fun f => by
      have p := not_congr (isIso_iff_nonzero f)
      simp only [Classical.not_not, Ne] at p
      exact p.mp fun _ => h (asIso f)
  finrank_zero_of_subsingleton

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
⊢ f = 0

Tactic:
have p := not_congr (isIso_iff_nonzero f)

Result:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ f = 0

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ f = 0

Tactic:
simp only [Classical.not_not, Ne] at p

Result:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0

Tactic:
exact p.mp fun _ => h (asIso f)

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem _root_.PrimrecPred.and {p q : α → Prop} [DecidablePred p] [DecidablePred q]
    (hp : PrimrecPred p) (hq : PrimrecPred q) : PrimrecPred fun a => p a ∧ q a :=
  (Primrec.and.comp hp hq).of_eq fun n => by simp

Proof state:
α : Type u_1
inst✝² : Primcodable α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : PrimrecPred p
hq : PrimrecPred q
n : α
⊢ (decide (p n) && decide (q n)) = decide ((fun a => p a ∧ q a) n)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Countable/Basic.lean
lemma countable_right_of_prod_of_nonempty [Nonempty α] (h : Countable (α × β)) : Countable β

Proof state:
α : Type u
β : Type v
inst✝ : Nonempty α
h : ¬Countable β
⊢ ¬Countable (α × β)

Tactic:
rw [not_countable_iff] at *

Result:
α : Type u
β : Type v
inst✝ : Nonempty α
h : Uncountable β
⊢ Uncountable (α × β)

Proof state:
α : Type u
β : Type v
inst✝ : Nonempty α
h : Uncountable β
⊢ Uncountable (α × β)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Nonempty α
h : Countable (α × β)
⊢ Countable β

Tactic:
contrapose h

Result:
α : Type u
β : Type v
inst✝ : Nonempty α
h : ¬Countable β
⊢ ¬Countable (α × β)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y

Proof state:
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ ∀ (s : σ), (x <* y).run s = (const β <$> x <*> y).run s

Tactic:
intro s

Result:
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (x <* y).run s = (const β <$> x <*> y).run s

Proof state:
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (x <* y).run s = (const β <$> x <*> y).run s

Tactic:
simp [←bind_pure_comp]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ x <* y = const β <$> x <*> y

Tactic:
apply ext

Result:
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ ∀ (s : σ), (x <* y).run s = (const β <$> x <*> y).run s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem mem_take_iff_getElem {l : List α} {a : α} :
    a ∈ l.take n ↔ ∃ (i : Nat) (hm : i < min n l.length), l[i] = a

Proof state:
case mpr
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i hm, l[i] = a) → ∃ i h, (take n l)[i] = a

Tactic:
rintro ⟨i, hm, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < min n l.length
⊢ ∃ i_1 h, (take n l)[i_1] = l[i]

Proof state:
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (take n l)[i] = a) ↔ ∃ i hm, l[i] = a

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (take n l)[i] = a) → ∃ i hm, l[i] = a

case mpr
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i hm, l[i] = a) → ∃ i h, (take n l)[i] = a

Proof state:
case mp
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (take n l)[i] = a) → ∃ i hm, l[i] = a

Tactic:
rintro ⟨i, hm, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < (take n l).length
⊢ ∃ i_1 hm_1, l[i_1] = (take n l)[i]

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < (take n l).length
⊢ ∃ i_1 hm_1, l[i_1] = (take n l)[i]

Tactic:
simp at hm

Result:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (take n l).length
hm : i < min n l.length
⊢ ∃ i_1 hm, l[i_1] = (take n l)[i]

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (take n l).length
hm : i < min n l.length
⊢ l[i] = (take n l)[i]

Tactic:
rw [getElem_take]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
a : α
⊢ a ∈ take n l ↔ ∃ i hm, l[i] = a

Tactic:
rw [mem_iff_getElem]

Result:
α : Type u_1
n : Nat
l : List α
a : α
⊢ (∃ i h, (take n l)[i] = a) ↔ ∃ i hm, l[i] = a

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (take n l).length
hm : i < min n l.length
⊢ i < min n l.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < min n l.length
⊢ ∃ i_1 h, (take n l)[i_1] = l[i]

Tactic:
refine ⟨i, by simpa, by rw [getElem_take]⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < min n l.length
⊢ i < (take n l).length

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
i : Nat
hm : i < min n l.length
⊢ (take n l)[i] = l[i]

Tactic:
rw [getElem_take]

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
l : List α
i : Nat
hm✝ : i < (take n l).length
hm : i < min n l.length
⊢ ∃ i_1 hm, l[i_1] = (take n l)[i]

Tactic:
refine ⟨i, by omega, by rw [getElem_take]⟩

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)] lemma leOnePart_eq_inv : a⁻ᵐ = a⁻¹ ↔ a ≤ 1

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = a⁻¹ ↔ a ≤ 1

Tactic:
simp [leOnePart]

Result:
no goals