harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
/-- The operator norm of the first projection `E × F → E` is exactly 1 if `E` is nontrivial. -/
@[simp] lemma norm_fst [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial E] :
    ‖fst 𝕜 E F‖ = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
⊢ ‖fst 𝕜 E F‖ = 1

Tactic:
refine le_antisymm (norm_fst_le ..) ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
⊢ 1 ≤ ‖fst 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ ‖fst 𝕜 E F‖ * ‖e‖
⊢ 1 ≤ ‖fst 𝕜 E F‖

Tactic:
rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ ‖fst 𝕜 E F‖ * (‖e‖ ⊔ ‖0‖)
⊢ 1 ≤ ‖fst 𝕜 E F‖

Tactic:
rw [norm_zero, max_eq_left (norm_nonneg e)] at this

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ ‖fst 𝕜 E F‖ * ‖e‖
⊢ 1 ≤ ‖fst 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
⊢ 1 ≤ ‖fst 𝕜 E F‖

Tactic:
let ⟨e, he⟩ := exists_ne (0 : E)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
⊢ 1 ≤ ‖fst 𝕜 E F‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
⊢ 1 ≤ ‖fst 𝕜 E F‖

Tactic:
have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ ‖fst 𝕜 E F‖ * (‖e‖ ⊔ ‖0‖)
⊢ 1 ≤ ‖fst 𝕜 E F‖
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_is_bilimit' {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPullback (0 : 0 ⟶ X) (0 : 0 ⟶ Y) b.inl b.inr

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 ≫ b.inl = 0 ≫ b.inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback (0 ≫ 0) 0 0 (b.inr ≫ b.snd)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 0 b.inl b.inr

Tactic:
refine IsPullback.of_right ?_ (by simp) (IsPullback.inl_snd' h).flip

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem mapIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
    (f : Nat → α → m β) :
    l.toArray.mapIdxM f = toArray <$> l.mapIdxM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ toArray <$> mapFinIdxM.go l (fun i a x => f i a) l #[] ⋯ = toArray <$> mapIdxM.go f l #[]

Tactic:
rw [go]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
bs : List α
acc : Array β
inv : [].length + acc.size = l.length
⊢ mapFinIdxM.go l (fun i a h => f i a) [] acc inv = mapIdxM.go f [] acc

Tactic:
simp only [mapFinIdxM.go, mapIdxM.go]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ (l.toArray.mapFinIdxM fun i a x => f i a) = toArray <$> mapIdxM f l

Tactic:
rw [mapFinIdxM_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ (toArray <$> l.mapFinIdxM fun i a x => f i a) = toArray <$> mapIdxM f l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ (toArray <$> l.mapFinIdxM fun i a x => f i a) = toArray <$> mapIdxM f l

Tactic:
simp only [mapFinIdxM, mapIdxM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ toArray <$> mapFinIdxM.go l (fun i a x => f i a) l #[] ⋯ = toArray <$> mapIdxM.go f l #[]

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
bs : List α
acc : Array β
inv : bs.length + acc.size = l.length
⊢ mapFinIdxM.go l (fun i a h => f i a) bs acc inv = mapIdxM.go f bs acc

Tactic:
match bs with
| [] => simp only [mapFinIdxM.go, mapIdxM.go]
| x :: xs => simp only [mapFinIdxM.go, mapIdxM.go, go]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ Array.mapIdxM f l.toArray = toArray <$> mapIdxM f l

Tactic:
unfold Array.mapIdxM

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
⊢ (l.toArray.mapFinIdxM fun i a x => f i a) = toArray <$> mapIdxM f l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : Nat → α → m β
bs : List α
acc : Array β
x : α
xs : List α
inv : (x :: xs).length + acc.size = l.length
⊢ mapFinIdxM.go l (fun i a h => f i a) (x :: xs) acc inv = mapIdxM.go f (x :: xs) acc

Tactic:
simp only [mapFinIdxM.go, mapIdxM.go, go]

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma fromSpecStalkOfMem_restrict (f : X.PartialMap Y)
    {U : X.Opens} (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) {x} (hx : x ∈ U) :
    (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem (hU' hx)

Proof state:
case e_a.e_a.e_f
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ ≫ inv (Hom.stalkMap U.ι ⟨x, hx⟩) =
    ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)

Tactic:
rw [Iso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq, IsIso.eq_inv_comp,
  stalkMap_congr_hom _ _ (X.homOfLE_ι hU').symm]

Result:
case e_a.e_a.e_f
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
e : ⟨x, ⋯⟩ = (ConcreteCategory.hom (X.homOfLE hU').base) ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem le_perfectClosure_iff (L : IntermediateField F E) :
    L ≤ perfectClosure F E ↔ IsPurelyInseparable F L

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : L ≤ perfectClosure F E
x : ↥L
n : ℕ
y : F
hy : (algebraMap F E) y = ↑x ^ ringExpChar F ^ n
⊢ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range

Tactic:
exact ⟨n, y, (algebraMap L E).injective hy⟩

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
⊢ L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L

Tactic:
refine ⟨fun h ↦ (isPurelyInseparable_iff_pow_mem F (ringExpChar F)).2 fun x ↦ ?_,
  fun _ ↦ le_perfectClosure F E L⟩

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : L ≤ perfectClosure F E
x : ↥L
⊢ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : L ≤ perfectClosure F E
x : ↥L
⊢ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range

Tactic:
obtain ⟨n, y, hy⟩ := h x.2

Result:
case intro.intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : L ≤ perfectClosure F E
x : ↥L
n : ℕ
y : F
hy : (algebraMap F E) y = ↑x ^ ringExpChar F ^ n
⊢ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
-- Mathlib/Topology/Algebra/Support.lean
theorem HasCompactSupport.mul_left (hf : HasCompactSupport f') : HasCompactSupport (f * f')

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f * f') x = 0 x

Tactic:
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f'
⊢ HasCompactSupport (f * f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Result:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_inv_neg_one {α} [DivisionRing α] : {a : α} →
    IsInt a (.negOfNat (nat_lit 1)) → IsInt a⁻¹ (.negOfNat (nat_lit 1))
  | _, ⟨rfl⟩ => ⟨by simp [inv_neg_one]⟩

Proof state:
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑(Int.negOfNat 1))⁻¹ = ↑(Int.negOfNat 1)

Tactic:
simp [inv_neg_one]

Result:
no goals
-- Mathlib/Algebra/Homology/Bifunctor.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctorDesc (i₁ : I₁) (i₂ : I₂) (h : ComplexShape.π c₁ c₂ c ⟨i₁, i₂⟩ = j) :
    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ mapBifunctorDesc f = f i₁ i₂ h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹⁰ : Category.{u_9, u_1} C₁
inst✝⁹ : Category.{u_8, u_2} C₂
inst✝⁸ : Category.{u_7, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝⁷ : HasZeroMorphisms C₁
inst✝⁶ : HasZeroMorphisms C₂
inst✝⁵ : Preadditive D
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : DecidableEq J
A : D
j : J
f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ mapBifunctorDesc f = f i₁ i₂ h

Tactic:
apply HomologicalComplex₂.ι_totalDesc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.replicate n []

Proof state:
case nil
α : Type u_1
⊢ Nonempty α ∨ ∃ n, [] = List.replicate n []

Tactic:
exact Or.inr ⟨0, rfl⟩

Result:
no goals

Proof state:
case inl.h
α : Type u_1
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α

Tactic:
exact h

Result:
no goals

Proof state:
case inr.intro.h
α : Type u_1
c : Clause α
n : Nat
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

Tactic:
exact ⟨n + 1, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
f : CNF α
⊢ Nonempty α ∨ ∃ n, f = List.replicate n []

Tactic:
induction f with
| nil => exact Or.inr ⟨0, rfl⟩
| cons c x ih => match c with
  | [] => cases ih with
    | inl h => left; exact h
    | inr h =>
      obtain ⟨n, rfl⟩ := h
      right
      exact ⟨n + 1, rfl⟩
  | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩

Result:
no goals

Proof state:
α : Type u_1
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []

Tactic:
cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
c : Clause α
n : Nat
⊢ Nonempty α ∨ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

Tactic:
right

Result:
case inr.intro.h
α : Type u_1
c : Clause α
n : Nat
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

Proof state:
case inr
α : Type u_1
c : Clause α
x : List (Clause α)
h : ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case inr.intro
α : Type u_1
c : Clause α
n : Nat
⊢ Nonempty α ∨ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

Proof state:
case cons
α : Type u_1
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, c :: x = List.replicate n []

Tactic:
match c with
| [] => cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩
| ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩

Result:
no goals

Proof state:
α : Type u_1
c✝ : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
a : α
b : Bool
c : List (Literal α)
⊢ Nonempty α ∨ ∃ n, ((a, b) :: c) :: x = List.replicate n []

Tactic:
exact Or.inl ⟨a⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α ∨ ∃ n, [] :: x = List.replicate n []

Tactic:
left

Result:
case inl.h
α : Type u_1
c : Clause α
x : List (Clause α)
h : Nonempty α
⊢ Nonempty α
-- Mathlib/GroupTheory/Solvable.lean
theorem Equiv.Perm.not_solvable (X : Type*) (hX : 5 ≤ Cardinal.mk X) :
    ¬IsSolvable (Equiv.Perm X)

Proof state:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ Nonempty (Fin 5 ↪ X)

Tactic:
rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]

Result:
no goals

Proof state:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
⊢ ¬IsSolvable (Perm X)

Tactic:
intro h

Result:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ False

Proof state:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False

Tactic:
exact
  Equiv.Perm.fin_5_not_solvable
    (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))

Result:
no goals

Proof state:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ False

Tactic:
have key : Nonempty (Fin 5 ↪ X) := by
  rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]

Result:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False
-- Mathlib/Algebra/Polynomial/Degree/Monomial.lean
theorem C_mul_X_pow_eq_self (h : #p.support ≤ 1) : C p.leadingCoeff * X ^ p.natDegree = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ C p.leadingCoeff * X ^ p.natDegree = p

Tactic:
rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_comap_of_surjective {f : α → β} (hf : Surjective f) (l : Filter β) :
    map f (comap f l) = l :=
  map_comap_of_mem <| by simp only [hf.range_eq, univ_mem]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
l : Filter β
⊢ range f ∈ l

Tactic:
simp only [hf.range_eq, univ_mem]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean
lemma isRatCondKernelCDFAux_density_Iic (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    IsRatCondKernelCDFAux (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ) where
  measurable := measurable_pi_iff.mpr fun _ ↦ measurable_density κ (fst κ) measurableSet_Iic
  mono' a q r hqr :=
    ae_of_all _ fun c ↦ density_mono_set le_rfl a c (Iic_subset_Iic.mpr (by exact_mod_cast hqr))
  nonneg' _ _ := ae_of_all _ fun _ ↦ density_nonneg le_rfl _ _ _
  le_one' _ _ := ae_of_all _ fun _ ↦ density_le_one le_rfl _ _ _
  tendsto_integral_of_antitone a s hs_anti hs_tendsto

Proof state:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : ↑q < x
⊢ ∃ x_1, ↑(s x_1) < x

Tactic:
obtain ⟨i, hi⟩ := hs_tendsto q

Result:
case refine_2.h.intro
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : ↑q < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ∃ x_1, ↑(s x_1) < x

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
q r : ℚ
hqr : q ≤ r
c : γ
⊢ ↑q ≤ ↑r

Tactic:
exact_mod_cast hqr

Result:
no goals

Proof state:
case refine_2.h.intro
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : x < ↑q
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
⊢ ↑q ≤ ↑(s i)

Tactic:
exact mod_cast hi i le_rfl

Result:
no goals

Proof state:
case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
⊢ ⋂ i, s' i = ∅

Tactic:
ext x

Result:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
⊢ x ∈ ⋂ i, s' i ↔ x ∈ ∅
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
    (x : B) (hx : Algebra.adjoin K {algebraMap B L x} = ⊤) :
    (conductor A x) * differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))}

Proof state:
case a.a.h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this✝¹ : IsFractionRing B L
y : L
hne₁ : (aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))) ≠ 0
this✝ : (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
hne₂ : ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ ≠ 0
this : IsIntegral A ((algebraMap B L) x)
⊢ (∀ (z : B), y * (algebraMap B L) z ∈ adjoin A {(algebraMap B L) x}) ↔
    ∀ a ∈ 1,
      ((traceForm K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * y)) a ∈ (algebraMap A K).range

Tactic:
simp_rw [← Subalgebra.mem_toSubmodule, ← Submodule.mul_mem_smul_iff (y := y * _)
  (mem_nonZeroDivisors_of_ne_zero hne₂)]

Result:
case a.a.h
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this✝¹ : IsFractionRing B L
y : L
hne₁ : (aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))) ≠ 0
this✝ : (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
hne₂ : ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ ≠ 0
this : IsIntegral A ((algebraMap B L) x)
⊢ (∀ (z : B),
      ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ * (y * (algebraMap B L) z) ∈
        ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ •
          Subalgebra.toSubmodule (adjoin A {(algebraMap B L) x})) ↔
    ∀ a ∈ 1,
      ((traceForm K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * y)) a ∈ (algebraMap A K).range
-- Mathlib/Data/PNat/Find.lean
theorem find_comp_succ (h : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h1 : ¬p 1) :
    PNat.find h = PNat.find h₂ + 1

Proof state:
case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
⊢ m + 1 < PNat.find h₂ + 1 → ¬p (m + 1)

Tactic:
intro hm

Result:
case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : m + 1 < PNat.find h₂ + 1
⊢ ¬p (m + 1)

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ PNat.find h = PNat.find h₂ + 1

Tactic:
refine (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩

Result:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ n < PNat.find h₂ + 1 → ¬p n

Proof state:
case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : ∀ m_1 ≤ m, ¬p (m_1 + 1)
⊢ ¬p (m + 1)

Tactic:
exact hm _ le_rfl

Result:
no goals

Proof state:
case one
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ 1 < PNat.find h₂ + 1 → ¬p 1

Tactic:
simp [h1]

Result:
no goals

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ n < PNat.find h₂ + 1 → ¬p n

Tactic:
induction n with
| one => simp [h1]
| succ m _ =>
  intro hm
  simp only [add_lt_add_iff_right, lt_find_iff] at hm
  exact hm _ le_rfl

Result:
no goals

Proof state:
case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : m + 1 < PNat.find h₂ + 1
⊢ ¬p (m + 1)

Tactic:
simp only [add_lt_add_iff_right, lt_find_iff] at hm

Result:
case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : ∀ m_1 ≤ m, ¬p (m_1 + 1)
⊢ ¬p (m + 1)