harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/LinearTopology.lean
/-- If a ring `R` is linearly ordered as a left *and* right module over itself,
then it has a basis of neighborhoods of zero made of *two-sided* ideals.

This is usually called a *linearly topologized ring*, but we do not add a specific spelling:
you should use `[IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R]` instead. -/
lemma hasBasis_twoSidedIdeal [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
    (𝓝 (0 : R)).HasBasis (fun I : TwoSidedIdeal R ↦ (I : Set R) ∈ 𝓝 0)
      (fun I : TwoSidedIdeal R ↦ (I : Set R)) :=
  hasBasis_subbimodule R Rᵐᵒᵖ |>.to_hasBasis
    (fun I ⟨hI, hRI, hRI'⟩ ↦ ⟨.mk' I (zero_mem _) add_mem neg_mem (hRI _ _) (hRI' _ _),
      by simpa using hI, by simp⟩)
    (fun I hI ↦ ⟨I.asIdeal.toAddSubgroup,
      ⟨hI, I.mul_mem_left, fun r x hx ↦ I.mul_mem_right x (r.unop) hx⟩, subset_rfl⟩)

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
x✝ : ↑I ∈ 𝓝 0 ∧ (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : ↑I ∈ 𝓝 0
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ ↑(TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯) ∈ 𝓝 0

Tactic:
simpa using hI

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
x✝ : ↑I ∈ 𝓝 0 ∧ (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : ↑I ∈ 𝓝 0
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ ↑(TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯) ⊆ ↑I

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithBot.ofDual_le_ofDual_iff {x y : WithBot αᵒᵈ} :
    WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Proof state:
α : Type u_1
inst✝ : LE α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem extend_restrict {x : FamilyOfElements P (generate R).arrows} (t : x.Compatible) :
    (x.restrict (le_generate R)).sieveExtend = x

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend = x

Tactic:
funext _ _ h

Result:
case h.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend x✝ h = x x✝ h

Proof state:
case h.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend x✝ h = x x✝ h

Tactic:
apply (t _ _ _).symm.trans

Result:
case h.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ x (⋯.choose ≫ ⋯.choose) ⋯ = x x✝ h

Proof state:
case h.h.h.e_f
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ ⋯.choose ≫ ⋯.choose = x✝

Tactic:
exact h.choose_spec.choose_spec.choose_spec.2

Result:
no goals

Proof state:
case h.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ x (⋯.choose ≫ ⋯.choose) ⋯ = x x✝ h

Tactic:
congr

Result:
case h.h.h.e_f
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ ⋯.choose ≫ ⋯.choose = x✝

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.Compatible
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend = x

Tactic:
rw [compatible_iff_sieveCompatible] at t

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend = x
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem Hereditarily.empty : Hereditarily p x → p ∅

Proof state:
case inl
p : ZFSet.{u} → Prop
x : ZFSet.{u}
IH : ∀ y ∈ ∅, Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅

Tactic:
exact h.self

Result:
no goals

Proof state:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x → p ∅

Tactic:
apply @ZFSet.inductionOn _ x

Result:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅

Proof state:
case inr.intro
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ y.toSet
⊢ p ∅

Tactic:
exact IH a ha (h.mem ha)

Result:
no goals

Proof state:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅

Tactic:
rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)

Result:
case inl
p : ZFSet.{u} → Prop
x : ZFSet.{u}
IH : ∀ y ∈ ∅, Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅

case inr.intro
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ y.toSet
⊢ p ∅

Proof state:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅

Tactic:
intro y IH h

Result:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Basic.lean
theorem merge_right (xs : List α) : merge xs [] le = xs

Proof state:
case cons
α : Type u_1
le : α → α → Bool
x : α
xs : List α
ih : xs.merge [] le = xs
⊢ (x :: xs).merge [] le = x :: xs

Tactic:
simp [merge, ih]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
xs : List α
⊢ xs.merge [] le = xs

Tactic:
induction xs with
| nil => simp [merge]
| cons x xs ih => simp [merge, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
le : α → α → Bool
⊢ [].merge [] le = []

Tactic:
simp [merge]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem not_dvd_card_commutator_or_not_dvd_index_commutator :
    ¬ p ∣ Nat.card (commutator G) ∨ ¬ p ∣ (commutator G).index

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_ <;>
    refine fun hP h ↦ P.not_dvd_index (h.trans ?_)

Result:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ (↑P).index

case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : ↑P ≤ commutator G
h : p ∣ (commutator G).index
⊢ (commutator G).index ∣ (↑P).index

Proof state:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker

Tactic:
exact Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ (↑P).index

Tactic:
rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]

Result:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker

Proof state:
case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : ↑P ≤ commutator G
h : p ∣ (commutator G).index
⊢ (commutator G).index ∣ (↑P).index

Tactic:
exact Subgroup.index_dvd_of_le hP

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem le_trailingDegree_C_mul_X_pow (n : ℕ) (a : R) :
    (n : ℕ∞) ≤ trailingDegree (C a * X ^ n)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ ((monomial n) a).trailingDegree

Tactic:
exact le_trailingDegree_monomial

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ (C a * X ^ n).trailingDegree

Tactic:
rw [C_mul_X_pow_eq_monomial]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ ((monomial n) a).trailingDegree
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Dense.Ioi_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :
    Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Proof state:
case intro.intro.intro
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
y : α
hys : y ∈ s
hxy : x < y
hyz : y < z
⊢ z ∈ ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
exact mem_iUnion₂.2 ⟨y, ⟨hys, hxy⟩, hyz⟩

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
⊢ z ∈ ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
rcases hs.exists_between hz with ⟨y, hys, hxy, hyz⟩

Result:
case intro.intro.intro
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
y : α
hys : y ∈ s
hxy : x < y
hyz : y < z
⊢ z ∈ ⋃ y ∈ s ∩ Ioi x, Ioi y

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x : α
⊢ Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))

Result:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x z : α
hz : z ∈ Ioi x
⊢ z ∈ ⋃ y ∈ s ∩ Ioi x, Ioi y
-- Mathlib/Data/Ordmap/Ordset.lean
theorem balancedSz_zero {l : ℕ} : BalancedSz l 0 ↔ l ≤ 1

Proof state:
l : ℕ
⊢ BalancedSz l 0 ↔ l ≤ 1

Tactic:
simp +contextual [BalancedSz]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem pi_principal [Finite ι] (s : (i : ι) → Set (α i)) :
    pi (fun i ↦ 𝓟 (s i)) = 𝓟 (univ.pi s)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
s : (i : ι) → Set (α i)
⊢ (pi fun i => 𝓟 (s i)) = 𝓟 (univ.pi s)

Tactic:
simp [Filter.pi, Set.pi_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Vector α n) (init : γ) :
    (l.filterMap f).foldlM g init =
      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
l : Array α
⊢ Array.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l =
    Array.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
l : Vector α n
init : γ
⊢ Array.foldlM g init (Array.filterMap f l.toArray) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
l : Array α
⊢ Array.foldlM g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
l : Array α
⊢ Array.foldlM g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldlM_filterMap]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
l : Array α
⊢ Array.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l =
    Array.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Filter.HasBasis.nhds_of_one {ι : Sort*} {p : ι → Prop} {s : ι → Set G}
    (hb : HasBasis (𝓝 1 : Filter G) p s) (x : G) :
    HasBasis (𝓝 x) p fun i => { y | y / x ∈ s i }

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i => {y | y * x⁻¹ ∈ s i}

Tactic:
exact hb.comap _

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i => {y | y / x ∈ s i}

Tactic:
simp_rw [div_eq_mul_inv]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i => {y | y * x⁻¹ ∈ s i}

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (𝓝 x).HasBasis p fun i => {y | y / x ∈ s i}

Tactic:
rw [← nhds_translation_mul_inv]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i => {y | y / x ∈ s i}
-- Mathlib/Data/Sym/Basic.lean
theorem sigma_sub_ext {m₁ m₂ : Σi : Fin (n + 1), Sym α (n - i)} (h : (m₁.2 : Multiset α) = m₂.2) :
    m₁ = m₂ :=
  Sigma.subtype_ext
    (Fin.ext <| by
      rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h,
        ← val_eq_coe, m₂.2.2, Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)])
    h

Proof state:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ ↑m₁.fst = ↑m₂.fst

Tactic:
rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h,
  ← val_eq_coe, m₂.2.2, Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma genWeightSpaceOf_ne_bot (χ : Weight R L M) (x : L) :
    genWeightSpaceOf M (χ x) x ≠ ⊥

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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥
⊢ genWeightSpaceOf M (χ x) x ≠ ⊥

Tactic:
contrapose! this

Result:
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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x = ⊥

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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
⊢ genWeightSpaceOf M (χ x) x ≠ ⊥

Tactic:
have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot

Result:
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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥
⊢ genWeightSpaceOf M (χ x) x ≠ ⊥

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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x ≤ ⊥

Tactic:
exact le_of_le_of_eq (iInf_le _ _) this

Result:
no goals

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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x = ⊥

Tactic:
rw [eq_bot_iff]

Result:
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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x ≤ ⊥
-- Mathlib/Combinatorics/SimpleGraph/Dart.lean
theorem dartOfNeighborSet_injective (v : V) : Function.Injective (G.dartOfNeighborSet v) :=
  fun e₁ e₂ h =>
  Subtype.ext <| by
    injection h with h'
    convert congr_arg Prod.snd h'

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : ↑(G.neighborSet v)
h : G.dartOfNeighborSet v e₁ = G.dartOfNeighborSet v e₂
⊢ ↑e₁ = ↑e₂

Tactic:
injection h with h'

Result:
V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : ↑(G.neighborSet v)
h' : (v, ↑e₁) = (v, ↑e₂)
⊢ ↑e₁ = ↑e₂

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : ↑(G.neighborSet v)
h' : (v, ↑e₁) = (v, ↑e₂)
⊢ ↑e₁ = ↑e₂

Tactic:
convert congr_arg Prod.snd h'

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem ofAdd_image_multiples_eq_powers_ofAdd [AddMonoid A] {x : A} :
    Multiplicative.ofAdd '' (AddSubmonoid.multiples x : Set A) =
      Submonoid.powers (Multiplicative.ofAdd x)

Proof state:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)

Tactic:
exact ofMul_image_powers_eq_multiples_ofMul

Result:
no goals

Proof state:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))

Tactic:
symm

Result:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)

Proof state:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)

Tactic:
rw [Equiv.eq_image_iff_symm_image_eq]

Result:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getLast_range (n : Nat) (h) : (range n).getLast h = n - 1

Proof state:
case zero
h : range 0 ≠ []
⊢ (range 0).getLast h = 0 - 1

Tactic:
simp at h

Result:
no goals

Proof state:
n : Nat
h : range n ≠ []
⊢ (range n).getLast h = n - 1

Tactic:
cases n with
| zero => simp at h
| succ n => simp [getLast?_range, getLast_eq_iff_getLast_eq_some]

Result:
no goals

Proof state:
case succ
n : Nat
h : range (n + 1) ≠ []
⊢ (range (n + 1)).getLast h = n + 1 - 1

Tactic:
simp [getLast?_range, getLast_eq_iff_getLast_eq_some]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.of_mul_right {f g : R[X]} (h : (f * g).Separable) : g.Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (g * f).Separable
⊢ g.Separable

Tactic:
exact h.of_mul_left

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ g.Separable

Tactic:
rw [mul_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (g * f).Separable
⊢ g.Separable
-- Mathlib/Topology/Sets/Compacts.lean
theorem coe_finset_sup {ι : Type*} {s : Finset ι} {f : ι → Compacts α} :
    (↑(s.sup f) : Set α) = s.sup fun i => ↑(f i)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i => ↑(f i)
⊢ ↑((Finset.cons a s x✝).sup f) = (Finset.cons a s x✝).sup fun i => ↑(f i)

Tactic:
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i => ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ∪ s.sup fun i => ↑(f i)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i => ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ∪ s.sup fun i => ↑(f i)

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ ↑(s.sup f) = s.sup fun i => ↑(f i)

Tactic:
refine Finset.cons_induction_on s rfl fun a s _ h => ?_

Result:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i => ↑(f i)
⊢ ↑((Finset.cons a s x✝).sup f) = (Finset.cons a s x✝).sup fun i => ↑(f i)
-- Mathlib/Data/Finset/Image.lean
lemma image_ssubset_image {t : Finset α} (hf : Injective f) : s.image f ⊂ t.image f ↔ s ⊂ t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s ⊂ image f t ↔ s ⊂ t

Tactic:
simp_rw [← lt_iff_ssubset]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s < image f t ↔ s < t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s < image f t ↔ s < t

Tactic:
exact lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)

Result:
no goals