harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem LinearMap.finrank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R]
    [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R L'] {s : S}
    (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') :
    Module.finrank R L ≤ Module.finrank R L'

Proof state:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_1
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ ↑(finrank R ↥L') < ℵ₀

Tactic:
exact nat_lt_aleph0 (finrank R ↥L')

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_1
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ finrank R ↥L ≤ finrank R ↥L'

Tactic:
refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_

Result:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_1
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ Module.rank R ↥L' < ℵ₀

Proof state:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_1
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ Module.rank R ↥L' < ℵ₀

Tactic:
rw [← Module.finrank_eq_rank R L']

Result:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_1
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ ↑(finrank R ↥L') < ℵ₀
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.disjoint_map_compl {s : Finset α} (hs : (s : Set α).Intersecting) :
    Disjoint s (s.map ⟨compl, compl_injective⟩)

Proof state:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
⊢ ∀ ⦃a : α⦄, a ∈ s → a ∉ map { toFun := compl, inj' := ⋯ } s

Tactic:
rintro x hx hxc

Result:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False

Proof state:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False

Tactic:
obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc

Result:
case intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx' : x ∈ s
hx : { toFun := compl, inj' := ⋯ } x ∈ s
hxc : { toFun := compl, inj' := ⋯ } x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False

Proof state:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
⊢ Disjoint s (map { toFun := compl, inj' := ⋯ } s)

Tactic:
rw [Finset.disjoint_left]

Result:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
⊢ ∀ ⦃a : α⦄, a ∈ s → a ∉ map { toFun := compl, inj' := ⋯ } s

Proof state:
case intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
x : α
hx' : x ∈ s
hx : { toFun := compl, inj' := ⋯ } x ∈ s
hxc : { toFun := compl, inj' := ⋯ } x ∈ map { toFun := compl, inj' := ⋯ } s
⊢ False

Tactic:
exact hs.not_compl_mem hx' hx

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem upperClosure_image (f : α ≃o β) :
    upperClosure (f '' s) = UpperSet.map f (upperClosure s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)

Tactic:
rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f.symm).symm (upperClosure s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f.symm).symm (upperClosure s)

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(upperClosure (⇑f '' s)) ↔ x✝ ∈ ↑((UpperSet.map f.symm).symm (upperClosure s))

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(upperClosure (⇑f '' s)) ↔ x✝ ∈ ↑((UpperSet.map f.symm).symm (upperClosure s))

Tactic:
simp [-UpperSet.symm_map, UpperSet.map, OrderIso.symm, ← f.le_symm_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem right_le_sup (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) : g ≤ f.sup g h

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
⊢ g ≤ f.sup g h

Tactic:
refine ⟨le_sup_right, fun z₁ z₂ hz => ?_⟩

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑g z₁ = ↑(f.sup g h) z₂

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑0 + ↑z₁ = ↑z₂

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑g z₁ = ↑(f.sup g h) z₂

Tactic:
rw [← zero_add (g _), ← f.map_zero]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f 0 + ↑g z₁ = ↑(f.sup g h) z₂

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f 0 + ↑g z₁ = ↑(f.sup g h) z₂

Tactic:
refine (sup_apply h _ _ _ ?_).symm

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑0 + ↑z₁ = ↑z₂
-- Mathlib/GroupTheory/GroupAction/Defs.lean
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.
Phrased as a set union. See `MulAction.selfEquivSigmaOrbits` for the type isomorphism. -/
@[to_additive "Decomposition of a type `X` as a disjoint union of its orbits under an additive group
action. Phrased as a set union. See `AddAction.selfEquivSigmaOrbits` for the type isomorphism."]
lemma univ_eq_iUnion_orbit :
    Set.univ (α := α) = ⋃ x : Ω, x.orbit

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ x ∈ Set.univ ↔ x ∈ ⋃ x, x.orbit

Tactic:
simp only [Set.mem_univ, Set.mem_iUnion, true_iff]

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ ∃ i, x ∈ i.orbit

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ ∃ i, x ∈ i.orbit

Tactic:
exact ⟨Quotient.mk'' x, by simp⟩

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ Set.univ = ⋃ x, x.orbit

Tactic:
ext x

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ x ∈ Set.univ ↔ x ∈ ⋃ x, x.orbit

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ x ∈ orbitRel.Quotient.orbit (Quotient.mk'' x)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem not_wellFounded_of_decreasing_seq (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) : ¬WellFounded r

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 => x1 > x2) ↪r r
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r r)

Tactic:
exact ⟨f⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 => x1 > x2) ↪r r
⊢ ¬WellFounded r

Tactic:
rw [wellFounded_iff_no_descending_seq, not_isEmpty_iff]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 => x1 > x2) ↪r r
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r r)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_append_of_ne_nil {α : Type u} {l : List α} :
    ∀ (l' : List α) (_ : l ≠ []), (l' ++ l).dropLast = l' ++ l.dropLast
  | [], _ => by simp only [nil_append]
  | a :: l', h => by
    rw [cons_append, dropLast, dropLast_append_of_ne_nil l' h, cons_append]
    simp [h]

Proof state:
case x_1
α : Type u
l : List α
a : α
l' : List α
h : l ≠ []
⊢ l' ++ l = [] → False

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
l : List α
x✝ : l ≠ []
⊢ ([] ++ l).dropLast = [] ++ l.dropLast

Tactic:
simp only [nil_append]

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
l' : List α
h : l ≠ []
⊢ (a :: l' ++ l).dropLast = a :: l' ++ l.dropLast

Tactic:
rw [cons_append, dropLast, dropLast_append_of_ne_nil l' h, cons_append]

Result:
case x_1
α : Type u
l : List α
a : α
l' : List α
h : l ≠ []
⊢ l' ++ l = [] → False
-- Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
theorem of_comp [SurjectiveOnStalks (f ≫ g)] : SurjectiveOnStalks f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↑↑X.toPresheafedSpace
this : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
rw [Scheme.stalkMap_comp] at this

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↑↑X.toPresheafedSpace
this :
  Function.Surjective
    ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
have := (f ≫ g).stalkMap_surjective x

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↑↑X.toPresheafedSpace
this : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
⊢ SurjectiveOnStalks f

Tactic:
refine ⟨fun x ↦ ?_⟩

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
x : ↑↑X.toPresheafedSpace
this :
  Function.Surjective
    ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
exact Function.Surjective.of_comp this

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

Tactic:
rfl

Result:
no goals

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.foldrM g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldrM_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.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l =
    Array.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l

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.foldrM g init (Array.filterMap f l.toArray) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      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.foldrM g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init { toArray := l, size_toArray := ⋯ }
-- Mathlib/FieldTheory/IntermediateField/Algebraic.lean
theorem eq_of_le_of_finrank_le'' [FiniteDimensional K L] (h_le : F ≤ E)
    (h_finrank : finrank F L ≤ finrank E L) : F = E

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E

Tactic:
apply eq_of_le_of_finrank_le h_le

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ finrank K ↥E ≤ finrank K ↥F

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ finrank K ↥E ≤ finrank K ↥F

Tactic:
have h1 := finrank_mul_finrank K F L

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank K ↥F * finrank (↥F) L = finrank K L
⊢ finrank K ↥E ≤ finrank K ↥F

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank K ↥F * finrank (↥F) L = finrank K L
h2 : finrank K ↥E * finrank (↥E) L = finrank K L
⊢ finrank K ↥E ≤ finrank K ↥F

Tactic:
have h3 : 0 < finrank E L := finrank_pos

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank K ↥F * finrank (↥F) L = finrank K L
h2 : finrank K ↥E * finrank (↥E) L = finrank K L
h3 : 0 < finrank (↥E) L
⊢ finrank K ↥E ≤ finrank K ↥F

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank K ↥F * finrank (↥F) L = finrank K L
h2 : finrank K ↥E * finrank (↥E) L = finrank K L
h3 : 0 < finrank (↥E) L
⊢ finrank K ↥E ≤ finrank K ↥F

Tactic:
nlinarith

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank K ↥F * finrank (↥F) L = finrank K L
⊢ finrank K ↥E ≤ finrank K ↥F

Tactic:
have h2 := finrank_mul_finrank K E L

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank K ↥F * finrank (↥F) L = finrank K L
h2 : finrank K ↥E * finrank (↥E) L = finrank K L
⊢ finrank K ↥E ≤ finrank K ↥F
-- Mathlib/CategoryTheory/Abelian/Injective/Basic.lean
theorem injective_of_preservesFiniteColimits_preadditiveYonedaObj (J : C)
    [hP : PreservesFiniteColimits (preadditiveYonedaObj J)] : Injective J

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Injective J

Tactic:
rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
this : (preadditiveYonedaObj J).PreservesHomology
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
have := Functor.preservesHomologyOfExact (preadditiveYonedaObj J)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
this : (preadditiveYonedaObj J).PreservesHomology
⊢ (preadditiveYonedaObj J).PreservesEpimorphisms
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_span_singleton [Module.Finite ℚ K] (x : K) :
    absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ x)|

Proof state:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑((Algebra.norm ℤ) r).natAbs / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

Tactic:
simp_rw [Int.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
  (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]

Result:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ |(Algebra.norm ℚ) ((algebraMap R K) r)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

Tactic:
obtain ⟨d, ⟨r, hr⟩⟩ := IsLocalization.exists_integer_multiple R⁰ x

Result:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem linearIndependent_right_of_flat (H : A.LinearDisjoint B) [Module.Flat R A]
    {ι : Type*} {b : ι → B} (hb : LinearIndependent R b) :
    LinearIndependent A (B.val ∘ b)

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Module.Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
have h := Submodule.LinearDisjoint.linearIndependent_right_of_flat H hb

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Module.Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h : LinearMap.ker ((toSubmodule A).mulRightMap b) = ⊥
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Module.Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h : LinearMap.ker ((toSubmodule A).mulRightMap b) = ⊥
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
rwa [mulRightMap_ker_eq_bot_iff_linearIndependent] at h

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[reassoc (attr := simp)]
lemma map_toSpecMvPoly {S T : Scheme.{max u v}} (f : S ⟶ T) :
    map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S

Proof state:
case a.h
n : Type v
S T : Scheme
f : S ⟶ T
i : n
⊢ (toSpecMvPolyIntEquiv n) (map n f ≫ toSpecMvPoly n T) i = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i

Tactic:
rw [toSpecMvPolyIntEquiv_comp, ← coord, map_appTop_coord, coord]

Result:
no goals

Proof state:
case a
n : Type v
S T : Scheme
f : S ⟶ T
⊢ (toSpecMvPolyIntEquiv n) (map n f ≫ toSpecMvPoly n T) = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S)

Tactic:
ext i

Result:
case a.h
n : Type v
S T : Scheme
f : S ⟶ T
i : n
⊢ (toSpecMvPolyIntEquiv n) (map n f ≫ toSpecMvPoly n T) i = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i

Proof state:
n : Type v
S T : Scheme
f : S ⟶ T
⊢ map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S

Tactic:
apply (toSpecMvPolyIntEquiv _).injective

Result:
case a
n : Type v
S T : Scheme
f : S ⟶ T
⊢ (toSpecMvPolyIntEquiv n) (map n f ≫ toSpecMvPoly n T) = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S)