harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Independence/Kernel.lean
theorem indepSets_singleton_iff {s t : Set Ω} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} :
    IndepSets {s} {t} κ μ ↔ ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t :=
  ⟨fun h ↦ h s t rfl rfl,
   fun h s1 t1 hs1 ht1 ↦ by rwa [Set.mem_singleton_iff.mp hs1, Set.mem_singleton_iff.mp ht1]⟩

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
s1 t1 : Set Ω
hs1 : s1 ∈ {s}
ht1 : t1 ∈ {t}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s1 ∩ t1) = (κ a) s1 * (κ a) t1

Tactic:
rwa [Set.mem_singleton_iff.mp hs1, Set.mem_singleton_iff.mp ht1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x y) < 2^n

Proof state:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : y = 0
⊢ (if x = 0 then if f false true = true then y else 0
    else
      if y = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := y / 2;
        let b₁ := x % 2 = 1;
        let b₂ := y % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) <
    2 ^ (n + 1)

Tactic:
simp only [x_zero, y_zero, if_neg, if_pos]

Result:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : y = 0
⊢ (if False then if f false true = true then 0 else 0 else if f true false = true then x else 0) < 2 ^ (n + 1)
-- Mathlib/Order/InitialSeg.lean
theorem mem_range_of_le [Preorder α] (f : α ≤i β) (h : b ≤ f a) : b ∈ Set.range f

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : f a ≤ f a
⊢ f a ∈ Set.range ⇑f

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
hb : b < f a
⊢ b ∈ Set.range ⇑f

Tactic:
exacts [⟨a, rfl⟩, f.mem_range_of_rel hb]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
⊢ b ∈ Set.range ⇑f

Tactic:
obtain rfl | hb := h.eq_or_lt

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : f a ≤ f a
⊢ f a ∈ Set.range ⇑f

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
hb : b < f a
⊢ b ∈ Set.range ⇑f
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_prod_isSolvable {s : Multiset F[X]} (hs : ∀ p ∈ s, IsSolvable (Gal p)) :
    IsSolvable s.prod.Gal

Proof state:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : IsSolvable t.prod.Gal
⊢ IsSolvable (p * t.prod).Gal

Tactic:
exact gal_mul_isSolvable (hs p hps) ht

Result:
no goals

Proof state:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]}, a ∈ s → s_1 ⊆ s → IsSolvable s_1.prod.Gal → IsSolvable (insert a s_1).prod.Gal

Tactic:
intro p t hps _ ht

Result:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : IsSolvable t.prod.Gal
⊢ IsSolvable (insert p t).prod.Gal

Proof state:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : IsSolvable t.prod.Gal
⊢ IsSolvable (insert p t).prod.Gal

Tactic:
rw [Multiset.insert_eq_cons, Multiset.prod_cons]

Result:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : IsSolvable t.prod.Gal
⊢ IsSolvable (p * t.prod).Gal

Proof state:
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
⊢ IsSolvable s.prod.Gal

Tactic:
apply Multiset.induction_on' s

Result:
case h₁
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
⊢ IsSolvable (Multiset.prod 0).Gal

case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]}, a ∈ s → s_1 ⊆ s → IsSolvable s_1.prod.Gal → IsSolvable (insert a s_1).prod.Gal

Proof state:
case h₁
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable p.Gal
⊢ IsSolvable (Multiset.prod 0).Gal

Tactic:
exact gal_one_isSolvable

Result:
no goals
-- Mathlib/FieldTheory/CardinalEmb.lean
lemma eq_bot_of_not_nonempty (hi : ¬ Nonempty (Iio i)) : filtration i = ⊥

Proof state:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(range WithTop.some)
this : Nonempty (Module.rank F E).ord.toType
⊢ filtration ⊤ = ⊥

Tactic:
exact (hi inferInstance).elim

Result:
no goals

Proof state:
case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.toType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥

Tactic:
exact bot_unique <| adjoin_le_iff.mpr fun _ ⟨j, hj, _⟩ ↦ (hi ⟨j, coe_lt_coe.mpr hj⟩).elim

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.toType
hi✝ : IsSuccPrelimit i
hi : ¬Nonempty ↑(Iio i)
⊢ filtration i = ⊥

Tactic:
cases i

Result:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
⊢ filtration ⊤ = ⊥

case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.toType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥

Proof state:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
⊢ filtration ⊤ = ⊥

Tactic:
have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'

Result:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
this : Nonempty (Module.rank F E).ord.toType
⊢ filtration ⊤ = ⊥

Proof state:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
this : Nonempty (Module.rank F E).ord.toType
⊢ filtration ⊤ = ⊥

Tactic:
rw [← range_coe] at hi

Result:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(range WithTop.some)
this : Nonempty (Module.rank F E).ord.toType
⊢ filtration ⊤ = ⊥
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_preOmega {o : Ordinal} (ho : IsSuccPrelimit o) : (preOmega o).cof = o.cof

Proof state:
case pos
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : IsMin o
⊢ (preOmega o).cof = o.cof

Tactic:
simp [h.eq_bot]

Result:
no goals

Proof state:
case neg
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ (preOmega o).cof = o.cof

Tactic:
exact isNormal_preOmega.cof_eq ⟨h, ho⟩

Result:
no goals

Proof state:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ (preOmega o).cof = o.cof

Tactic:
by_cases h : IsMin o

Result:
case pos
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : IsMin o
⊢ (preOmega o).cof = o.cof

case neg
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ (preOmega o).cof = o.cof
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
    (x.rotateLeft r).getLsbD i =
      cond (i < r)
      (x.getLsbD (w - r + i))
      (decide (i < w) && x.getLsbD (i - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hr : r < w
⊢ (x.rotateLeftAux r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

Tactic:
by_cases h : i < r

Result:
case pos
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : i < r
⊢ (x.rotateLeftAux r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

case neg
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : ¬i < r
⊢ (x.rotateLeftAux r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

Proof state:
case pos
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : i < r
⊢ (x.rotateLeftAux r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

Tactic:
simp [h, getLsbD_rotateLeftAux_of_le h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hr : r < w
⊢ (x.rotateLeft r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

Tactic:
rw [rotateLeft_eq_rotateLeftAux_of_lt hr]

Result:
w : Nat
x : BitVec w
r i : Nat
hr : r < w
⊢ (x.rotateLeftAux r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

Proof state:
case neg
w : Nat
x : BitVec w
r i : Nat
hr : r < w
h : ¬i < r
⊢ (x.rotateLeftAux r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

Tactic:
simp [h, getLsbD_rotateLeftAux_of_geq <| Nat.ge_of_not_lt h]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem mclosure_isSwap [Finite α] : Submonoid.closure { σ : Perm α | IsSwap σ } = ⊤

Proof state:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ x ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
rw [← h1]

Result:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
⊢ Submonoid.closure {σ | σ.IsSwap} = ⊤

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
⊢ Submonoid.closure {σ | σ.IsSwap} = ⊤

Proof state:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
exact Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)

Result:
no goals

Proof state:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
⊢ x ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
obtain ⟨h1, h2⟩ := Subtype.mem (truncSwapFactors x).out

Result:
case intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ x ∈ Submonoid.closure {σ | σ.IsSwap}

Proof state:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
⊢ Submonoid.closure {σ | σ.IsSwap} = ⊤

Tactic:
refine top_unique fun x _ ↦ ?_

Result:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
⊢ x ∈ Submonoid.closure {σ | σ.IsSwap}
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma LeftHomologyData.mapCyclesIso_eq [S.HasLeftHomology]
    [F.PreservesLeftHomologyOf S] :
    S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm

Proof state:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ cyclesMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.leftHomologyData.map F) =
    cyclesMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F) ≫ F.map (cyclesMap' (𝟙 S) hl S.leftHomologyData)

Tactic:
simp only [map_cyclesMap', ← cyclesMap'_comp, Functor.map_id, comp_id,
  Functor.mapShortComplex_obj]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm

Tactic:
ext

Result:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapCyclesIso F).hom = ((hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm).hom

Proof state:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapCyclesIso F).hom = ((hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm).hom

Tactic:
dsimp [mapCyclesIso, cyclesIso]

Result:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ cyclesMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.leftHomologyData.map F) =
    cyclesMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F) ≫ F.map (cyclesMap' (𝟙 S) hl S.leftHomologyData)
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_one : rescale 1 = RingHom.id R⟦X⟧

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ rescale 1 = RingHom.id R⟦X⟧

Tactic:
ext

Result:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff R n✝) ((rescale 1) x✝) = (coeff R n✝) ((RingHom.id R⟦X⟧) x✝)

Proof state:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff R n✝) ((rescale 1) x✝) = (coeff R n✝) ((RingHom.id R⟦X⟧) x✝)

Tactic:
simp only [coeff_rescale, one_pow, one_mul, RingHom.id_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem top_lie_le_iff_le_normalizer (N' : LieSubmodule R L M) :
    ⁅(⊤ : LieIdeal R L), N⁆ ≤ N' ↔ N ≤ N'.normalizer

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
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
N N' : LieSubmodule R L M
⊢ (∀ x ∈ ⊤, ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer

Tactic:
tauto

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
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
N N' : LieSubmodule R L M
⊢ ⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer

Tactic:
rw [lie_le_iff]

Result:
R : Type u_1
L : Type u_2
M : Type u_3
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
N N' : LieSubmodule R L M
⊢ (∀ x ∈ ⊤, ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
r s : ℝ
⊢ (↑(r + s)).re = (↑r + ↑s).re ∧ (↑(r + s)).im = (↑r + ↑s).im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p

Proof state:
p : Prop
d : Decidable p
⊢ decide p = true ↔ p

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem count_map_roots_of_injective [IsDomain A] [DecidableEq B] (p : A[X]) {f : A →+* B}
    (hf : Function.Injective f) (b : B) :
    (p.roots.map f).count b ≤ rootMultiplicity b (p.map f)

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero,
  rootMultiplicity_zero, le_refl]

Result:
no goals

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : ¬p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
exact count_map_roots ((Polynomial.map_ne_zero_iff hf).mpr hp0) b

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
by_cases hp0 : p = 0

Result:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : ¬p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)
-- Mathlib/RingTheory/CotangentLocalizationAway.lean
lemma compLocalizationAwayAlgHom_relation_eq_zero :
    compLocalizationAwayAlgHom T g P (rename Sum.inr (P.σ g) * X (Sum.inl ()) - 1) = 0

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ (compLocalizationAwayAlgHom T g P) ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) = 0

Tactic:
rw [map_sub, map_one, map_mul, ← toComp_toAlgHom (Generators.localizationAway g (S := T)) P]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway g).toComp P).toAlgHom (P.σ g)) *
        (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) -
      1 =
    0

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ (algebraMap (P.Ring ⧸ P.ker ^ 2) (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))))
          ((algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) (P.σ g)) *
        IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) -
      1 =
    0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway g).toComp P).toAlgHom (P.σ g)) *
        (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) -
      1 =
    0

Tactic:
rw [compLocalizationAwayAlgHom_toAlgHom_toComp, compLocalizationAwayAlgHom_X_inl,
  IsScalarTower.algebraMap_apply P.Ring (P.Ring ⧸ P.ker ^ 2) (Localization.Away _)]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ (algebraMap (P.Ring ⧸ P.ker ^ 2) (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))))
          ((algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) (P.σ g)) *
        IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) -
      1 =
    0
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_inter_ne_empty_iff {s t : Set α} {x : α} :
    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ (a * b⁻¹) • b = a

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h

Result:
case mp.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
rw [← nonempty_iff_ne_empty]

Result:
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Proof state:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ ((a * b⁻¹) • s ∩ t).Nonempty

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Proof state:
case mp.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
rintro ⟨a, h, ha⟩

Result:
case mp.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ x • b * b⁻¹ = x

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ ((a * b⁻¹) • s ∩ t).Nonempty

Tactic:
exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩

Result:
no goals