harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eq_one : #f.support = 1 ↔
    ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = C x * X ^ k

Proof state:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 1 → ℕ
x : Fin 1 → R
w✝ : StrictMono k
hx : ∀ (i : Fin 1), x i ≠ 0
h : #(∑ i : Fin 1, C (x i) * X ^ k i).support = 1
⊢ ∃ k_1 x_1, ∃ (_ : x_1 ≠ 0), ∑ i : Fin 1, C (x i) * X ^ k i = C x_1 * X ^ k_1

Tactic:
exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #(C x * X ^ k).support = 1

Tactic:
rw [support_C_mul_X_pow k hx, card_singleton]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 1
⊢ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

Tactic:
obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h

Result:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 1 → ℕ
x : Fin 1 → R
w✝ : StrictMono k
hx : ∀ (i : Fin 1), x i ≠ 0
h : #(∑ i : Fin 1, C (x i) * X ^ k i).support = 1
⊢ ∃ k_1 x_1, ∃ (_ : x_1 ≠ 0), ∑ i : Fin 1, C (x i) * X ^ k i = C x_1 * X ^ k_1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 1 ↔ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

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

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 1
⊢ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1

Tactic:
rintro ⟨k, x, hx, rfl⟩

Result:
case refine_2.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #(C x * X ^ k).support = 1
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem zero_of_le_dist (hx : f.rOut ≤ dist x c) : f x = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
⊢ ↑f x = 0

Tactic:
rwa [← nmem_support, support_eq, mem_ball, not_lt]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma integral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : α × β → E} (hf : Integrable f (μ ⊗ₘ κ)) :
    ∫ x, f x ∂(μ ⊗ₘ κ) = ∫ a, ∫ b, f (a, b) ∂(κ a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ ∫ (x : α), ∫ (y : β), f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ ∫ (x : α × β), f x ∂μ ⊗ₘ κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
rw [compProd, ProbabilityTheory.integral_compProd hf]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ ∫ (x : α), ∫ (y : β), f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem le_succ_rank_sUnion (x : PSet) : rank x ≤ succ (rank (⋃₀ x))

Proof state:
case h
x z : PSet.{u_1}
a✝ : z ∈ x
⊢ ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x

Tactic:
intro _ _

Result:
case h
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ z✝ ∈ ⋃₀ x

Proof state:
case h
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z

Tactic:
exists z

Result:
no goals

Proof state:
case h
x : PSet.{u_1}
⊢ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
intro z _

Result:
case h
x z : PSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset

Proof state:
case h
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ z✝ ∈ ⋃₀ x

Tactic:
rw [mem_sUnion]

Result:
case h
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z

Proof state:
case h
x z : PSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset

Tactic:
rw [mem_powerset, subset_iff]

Result:
case h
x z : PSet.{u_1}
a✝ : z ∈ x
⊢ ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x

Proof state:
x : PSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]

Result:
x : PSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank

Proof state:
case h
x : PSet.{u_1}
⊢ x ⊆ (⋃₀ x).powerset

Tactic:
rw [subset_iff]

Result:
case h
x : PSet.{u_1}
⊢ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset

Proof state:
x : PSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank

Tactic:
apply rank_mono

Result:
case h
x : PSet.{u_1}
⊢ x ⊆ (⋃₀ x).powerset
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS_even (m : ℤ) : preNormEDS b c d (2 * m) =
    preNormEDS b c d (m - 1) ^ 2 * preNormEDS b c d m * preNormEDS b c d (m + 2) -
      preNormEDS b c d (m - 2) * preNormEDS b c d m * preNormEDS b c d (m + 1) ^ 2

Proof state:
case nat.succ.succ.succ
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑(m + 1 + 1 + 1)) =
    preNormEDS b c d (↑(m + 1 + 1 + 1) - 1) ^ 2 * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 2) -
      preNormEDS b c d (↑(m + 1 + 1 + 1) - 2) * preNormEDS b c d ↑(m + 1 + 1 + 1) *
        preNormEDS b c d (↑(m + 1 + 1 + 1) + 1) ^ 2

Tactic:
simp only [Int.natCast_add, Nat.cast_one]

Result:
case nat.succ.succ.succ
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 1 + 1)) =
    preNormEDS b c d (↑m + 1 + 1 + 1 - 1) ^ 2 * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 2) -
      preNormEDS b c d (↑m + 1 + 1 + 1 - 2) * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 1) ^ 2

Proof state:
case nat.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑0) =
    preNormEDS b c d (↑0 - 1) ^ 2 * preNormEDS b c d ↑0 * preNormEDS b c d (↑0 + 2) -
      preNormEDS b c d (↑0 - 2) * preNormEDS b c d ↑0 * preNormEDS b c d (↑0 + 1) ^ 2

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem natCast_le_iff {m n : ℕ} : (m : EReal) ≤ (n : EReal) ↔ m ≤ n

Proof state:
m n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} : k ≤ 0 ↔ k = 0 :=
  ⟨fun h => Fin.ext <| by rw [Nat.eq_zero_of_le_zero h]; rfl, by rintro rfl; exact Nat.le_refl _⟩

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0

Tactic:
rw [Nat.eq_zero_of_le_zero h]

Result:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k = 0 → k ≤ 0

Tactic:
rintro rfl

Result:
n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mul_mem_cancel_right {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hg : g ∈ S.arrows d e) :
    f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
exact fun hf => S.mul hf hg

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d

case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
this : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d

Tactic:
simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d

Tactic:
apply S.mul h (S.inv hg)

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ f ∈ S.arrows c d

Tactic:
suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
  simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d

Tactic:
rintro h

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ f ∈ S.arrows c d
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval_one_map (f : R →+* S) (p : R[X]) : (p.map f).eval 1 = f (p.eval 1)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ eval 1 (map f p) = f (eval 1 p)

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r =>
  simp only [one_pow, mul_one, eval_monomial, map_monomial]

Result:
no goals

Proof state:
case h_monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
⊢ eval 1 (map f ((monomial n) r)) = f (eval 1 ((monomial n) r))

Tactic:
simp only [one_pow, mul_one, eval_monomial, map_monomial]

Result:
no goals

Proof state:
case h_add
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p q : R[X]
hp : eval 1 (map f p) = f (eval 1 p)
hq : eval 1 (map f q) = f (eval 1 q)
⊢ eval 1 (map f (p + q)) = f (eval 1 (p + q))

Tactic:
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.dense_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} :
    Dense s ↔ ∀ o ∈ b, Set.Nonempty o → (o ∩ s).Nonempty

Proof state:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
simp only [Dense, hb.mem_closure_iff]

Result:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Proof state:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
theorem whiskerRight_naturality_naturality {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') :
    F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
      η.naturality f ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ _ _ _).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : OplaxNatTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@[reassoc]
lemma ProjectiveResolution.isoLeftDerivedObj_hom_naturality
    {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f)
    (F : C ⥤ D) [F.Additive] (n : ℕ) :
    (F.leftDerived n).map f ≫ (Q.isoLeftDerivedObj F n).hom =
      (P.isoLeftDerivedObj F n).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (F.leftDerived n).map f ≫ (Q.isoLeftDerivedObj F n).hom =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        φ

Tactic:
dsimp [isoLeftDerivedObj, Functor.leftDerived]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (Q.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem alternatingGroup_le_of_index_le_two
    {G : Subgroup (Equiv.Perm α)} (hG : G.index ≤ 2) :
    alternatingGroup α ≤ G

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : G.index = Nat.succ 0
⊢ alternatingGroup α ≤ G

Tactic:
exact index_eq_one.mp h ▸ le_top

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index > 0
⊢ alternatingGroup α ≤ G

Tactic:
rcases (Nat.succ_le_iff.mpr h).eq_or_gt with h | h

Result:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : G.index = Nat.succ 0
⊢ alternatingGroup α ≤ G

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G

Tactic:
rw [eq_alternatingGroup_of_index_eq_two (hG.antisymm h)]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index = 0
⊢ alternatingGroup α ≤ G

Tactic:
exact (index_ne_zero_of_finite h).elim

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
⊢ alternatingGroup α ≤ G

Tactic:
rcases G.index.eq_zero_or_pos with h | h

Result:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index = 0
⊢ alternatingGroup α ≤ G

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index > 0
⊢ alternatingGroup α ≤ G
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem smulRight_one_one (c : R₁ →L[R₁] M₂) : smulRight (1 : R₁ →L[R₁] R₁) (c 1) = c

Proof state:
case h
R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ (smulRight 1 (c 1)) 1 = c 1

Tactic:
simp [← ContinuousLinearMap.map_smul_of_tower]

Result:
no goals

Proof state:
R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ smulRight 1 (c 1) = c

Tactic:
ext

Result:
case h
R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ (smulRight 1 (c 1)) 1 = c 1
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem zmultiplesHom_ker_eq [AddGroup G] (g : G) :
    (zmultiplesHom G g).ker = zmultiples ↑(addOrderOf g)

Proof state:
G : Type u_2
inst✝ : AddGroup G
g : G
⊢ ((zmultiplesHom G) g).ker = zmultiples ↑(addOrderOf g)

Tactic:
ext

Result:
case h
G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ x✝ ∈ ((zmultiplesHom G) g).ker ↔ x✝ ∈ zmultiples ↑(addOrderOf g)

Proof state:
case h
G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ x✝ ∈ ((zmultiplesHom G) g).ker ↔ x✝ ∈ zmultiples ↑(addOrderOf g)

Tactic:
simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
  ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem P_is_eventually_constant {q n : ℕ} (hqn : n ≤ q) :
    ((P (q + 1)).f n : X _⦋n⦌ ⟶ _) = (P q).f n

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hqn : 0 ≤ q
⊢ (P (q + 1)).f 0 = (P q).f 0

Tactic:
simp only [P_f_0_eq]

Result:
no goals

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n + 1 ≤ q
⊢ (P q).f (n + 1) ≫ (Hσ q).f (n + 1) = 0

Tactic:
exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ (P (q + 1)).f n = (P q).f n

Tactic:
cases n with
| zero => simp only [P_f_0_eq]
| succ n =>
  simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
    add_right_eq_self]
  exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)

Result:
no goals

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n + 1 ≤ q
⊢ (P (q + 1)).f (n + 1) = (P q).f (n + 1)

Tactic:
simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
  add_right_eq_self]

Result:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n + 1 ≤ q
⊢ (P q).f (n + 1) ≫ (Hσ q).f (n + 1) = 0
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem IsDecompOn.mono {f f' : X → X} {A A' : Set X} {S : Finset G} (h : IsDecompOn f A S)
    (hA' : A' ⊆ A) (hf' : EqOn f f' A') : IsDecompOn f' A' S

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f a = g • a

Tactic:
exact h a (hA' ha)

Result:
no goals

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
⊢ IsDecompOn f' A' S

Tactic:
intro a ha

Result:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f' a = g • a

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f' a = g • a

Tactic:
rw [← hf' ha]

Result:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f a = g • a
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem natDegree_eraseLead_le_of_nextCoeff_eq_zero (h : f.nextCoeff = 0) :
    f.eraseLead.natDegree ≤ f.natDegree - 2

Proof state:
case inr.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.nextCoeff = 0

Tactic:
simp [nextCoeff_eq_zero, h, eq_zero_or_pos]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 2

Tactic:
refine natDegree_le_pred (n := f.natDegree - 1) (eraseLead_natDegree_le f) ?_

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Proof state:
case inr.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
rw [eraseLead_coeff_of_ne _ (tsub_lt_self hf zero_lt_one).ne, ← nextCoeff_of_natDegree_pos hf]

Result:
case inr.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.nextCoeff = 0

Proof state:
case inl.intro
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).eraseLead.coeff ((C a).natDegree - 1) = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (∃ x, C x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h

Result:
case inl.intro
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).eraseLead.coeff ((C a).natDegree - 1) = 0

case inr.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
rw [nextCoeff_eq_zero, natDegree_eq_zero] at h

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (∃ x, C x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem powerlt_le {a b c : Cardinal.{u}} : a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Proof state:
case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c => a ^ ↑c)

Tactic:
rw [← image_eq_range]

Result:
case h
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)

Proof state:
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

Tactic:
simp

Result:
no goals

Proof state:
case h
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
exact bddAbove_image.{u, u} _ bddAbove_Iio

Result:
no goals

Proof state:
a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
rw [powerlt, ciSup_le_iff']

Result:
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c => a ^ ↑c)