harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem finite_of_algHom_finiteType_of_isJacobsonRing
    {K L A : Type*} [CommRing K] [Field L] [CommRing A]
    [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A]
    [Algebra K L] [Algebra K A]
    [Algebra.FiniteType K A] (f : L →ₐ[K] A) :
    Module.Finite K L

Proof state:
case intro
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this✝ : Field (A ⧸ m) := Quotient.field m
this : Module.Finite K (A ⧸ m)
⊢ Module.Finite K L

Tactic:
exact Module.Finite.of_injective ((Ideal.Quotient.mkₐ K m).comp f).toLinearMap
  (RingHom.injective _)

Result:
no goals

Proof state:
case intro
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this : Field (A ⧸ m) := Quotient.field m
⊢ Module.Finite K L

Tactic:
have := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)

Result:
case intro
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this✝ : Field (A ⧸ m) := Quotient.field m
this : Module.Finite K (A ⧸ m)
⊢ Module.Finite K L

Proof state:
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
⊢ Module.Finite K L

Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal A

Result:
case intro
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
⊢ Module.Finite K L

Proof state:
case intro
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
⊢ Module.Finite K L

Tactic:
letI := Ideal.Quotient.field m

Result:
case intro
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : Field L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this : Field (A ⧸ m) := Quotient.field m
⊢ Module.Finite K L
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem mul_coeff_one (p q : R[X]) :
    coeff (p * q) 1 = coeff p 0 * coeff q 1 + coeff p 1 * coeff q 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ map { toFun := fun i => (i, 1 - i), inj' := ⋯ } (range (1 + 1)), p.coeff x.1 * q.coeff x.2 =
    p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
simp [sum_range_succ]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
rw [coeff_mul, Nat.antidiagonal_eq_map]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ map { toFun := fun i => (i, 1 - i), inj' := ⋯ } (range (1 + 1)), p.coeff x.1 * q.coeff x.2 =
    p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_lt_of_nonneg_of_lt {a b n : α} (a_nonneg : 0 ≤ a) (a_lt_n : a < n)
    (b_nonneg : 0 ≤ b) (b_lt_n : b < n) : |a - b| < n

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b n : α
a_nonneg : 0 ≤ a
a_lt_n : a < n
b_nonneg : 0 ≤ b
b_lt_n : b < n
⊢ a < n + b ∧ b < n + a

Tactic:
exact ⟨lt_add_of_lt_of_nonneg a_lt_n b_nonneg, lt_add_of_lt_of_nonneg b_lt_n a_nonneg⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b n : α
a_nonneg : 0 ≤ a
a_lt_n : a < n
b_nonneg : 0 ≤ b
b_lt_n : b < n
⊢ |a - b| < n

Tactic:
rw [abs_sub_lt_iff, sub_lt_iff_lt_add, sub_lt_iff_lt_add]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b n : α
a_nonneg : 0 ≤ a
a_lt_n : a < n
b_nonneg : 0 ≤ b
b_lt_n : b < n
⊢ a < n + b ∧ b < n + a
-- Mathlib/Data/Seq/Seq.lean
theorem enum_cons (s : Seq α) (x : α) :
    enum (cons x s) = cons (0, x) (map (Prod.map Nat.succ id) (enum s))

Proof state:
case h.zero
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0

Tactic:
simp

Result:
no goals

Proof state:
case h.succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ (cons x s).enum.get? (n✝ + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n✝ + 1)

Tactic:
simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]

Result:
case h.succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ Option.map (Prod.mk (n✝ + 1)) (s.get? n✝) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n✝) (s.get? n✝)

Proof state:
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum = cons (0, x) (map (Prod.map Nat.succ id) s.enum)

Tactic:
ext ⟨n⟩ : 1

Result:
case h.zero
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0

case h.succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ (cons x s).enum.get? (n✝ + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n✝ + 1)

Proof state:
case h.succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ Option.map (Prod.mk (n✝ + 1)) (s.get? n✝) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n✝) (s.get? n✝)

Tactic:
congr

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Topology.lean
/-- The image of `Aut F` in `∀ X, Aut (F.obj X)` is closed. -/
lemma autEmbedding_range_isClosed : IsClosed (Set.range (autEmbedding F))

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ IsClosed (⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom})

Tactic:
refine isClosed_iInter (fun f ↦ isClosed_eq (X := F.obj f.left → F.obj f.right) ?_ ?_)

Result:
case refine_1
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a => F.map f.hom ≫ (a f.right).hom

case refine_2
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a => (a f.left).hom ≫ F.map f.hom

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a => F.map f.hom ≫ (a f.right).hom

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a => (a f.left).hom ≫ F.map f.hom

Tactic:
fun_prop

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ IsClosed (Set.range ⇑(autEmbedding F))

Tactic:
rw [autEmbedding_range]

Result:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ IsClosed (⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom})
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT {n : ℕ} {p : ℤ} (hp : Prime p) {a b c : ℤ}
    (hpa : p ∣ a) (hpb : p ∣ b) (HF : a ^ n + b ^ n + c ^ n = 0) : p ∣ c

Proof state:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
⊢ p ∣ c

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ p ∣ c

case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ c

Proof state:
case inl
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ p ∣ c

Tactic:
simp at HF

Result:
no goals

Proof state:
case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ c

Tactic:
refine hp.dvd_of_dvd_pow (n := n) (dvd_neg.1 ?_)

Result:
case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ -c ^ n

Proof state:
case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n = -c ^ n
hn : n ≠ 0
⊢ p ∣ -c ^ n

Tactic:
exact HF.symm ▸ dvd_add (dvd_pow hpa hn) (dvd_pow hpb hn)

Result:
no goals

Proof state:
case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ -c ^ n

Tactic:
rw [add_eq_zero_iff_eq_neg] at HF

Result:
case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n = -c ^ n
hn : n ≠ 0
⊢ p ∣ -c ^ n
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma IsUnit.prod_iff [CommMonoid β] : IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)

Proof state:
case empty
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
⊢ IsUnit (∏ a ∈ ∅, f a) ↔ ∀ a ∈ ∅, IsUnit (f a)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_3
β : Type u_4
s✝ : Finset α
f : α → β
inst✝ : CommMonoid β
a : α
s : Finset α
ha : a ∉ s
hs : IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)
⊢ IsUnit (∏ a ∈ Finset.cons a s ha, f a) ↔ ∀ a_1 ∈ Finset.cons a s ha, IsUnit (f a_1)

Tactic:
rw [Finset.prod_cons, IsUnit.mul_iff, hs, Finset.forall_mem_cons]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
⊢ IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha hs => rw [Finset.prod_cons, IsUnit.mul_iff, hs, Finset.forall_mem_cons]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem card_zpowers_le (a : G) {k : ℕ} (k_pos : k ≠ 0)
    (ha : a ^ k = 1) : Fintype.card (Subgroup.zpowers a) ≤ k

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ card ↥(zpowers a) ≤ k

Tactic:
rw [Fintype.card_zpowers]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ orderOf a ≤ k

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ orderOf a ≤ k

Tactic:
apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_append {K L : Array α} {f : (i : Nat) → α → (h : i < (K ++ L).size) → β} :
    (K ++ L).mapFinIdx f =
      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
        L.mapFinIdx (fun i a h => f (i + K.size) a (by simp; omega))

Proof state:
α : Type ?u.52380
β : Type ?u.52470
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
i : Nat
a : α
h : i < L.size
⊢ i + K.size < K.size + L.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.52380
β : Type ?u.52470
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
i : Nat
a : α
h : i < K.size
⊢ i < K.size + L.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
⊢ (K ++ L).mapFinIdx f = (K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.size) a ⋯

Tactic:
cases K

Result:
case mk
α : Type u_1
β : Type u_2
L : Array α
toList✝ : List α
f : (i : Nat) → α → i < ({ toList := toList✝ } ++ L).size → β
⊢ ({ toList := toList✝ } ++ L).mapFinIdx f =
    ({ toList := toList✝ }.mapFinIdx fun i a h => f i a ⋯) ++
      L.mapFinIdx fun i a h => f (i + { toList := toList✝ }.size) a ⋯

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ toList✝ : List α
f : (i : Nat) → α → i < ({ toList := toList✝¹ } ++ { toList := toList✝ }).size → β
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).mapFinIdx f =
    ({ toList := toList✝¹ }.mapFinIdx fun i a h => f i a ⋯) ++
      { toList := toList✝ }.mapFinIdx fun i a h => f (i + { toList := toList✝¹ }.size) a ⋯

Tactic:
simp [List.mapFinIdx_append]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
L : Array α
toList✝ : List α
f : (i : Nat) → α → i < ({ toList := toList✝ } ++ L).size → β
⊢ ({ toList := toList✝ } ++ L).mapFinIdx f =
    ({ toList := toList✝ }.mapFinIdx fun i a h => f i a ⋯) ++
      L.mapFinIdx fun i a h => f (i + { toList := toList✝ }.size) a ⋯

Tactic:
cases L

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ toList✝ : List α
f : (i : Nat) → α → i < ({ toList := toList✝¹ } ++ { toList := toList✝ }).size → β
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).mapFinIdx f =
    ({ toList := toList✝¹ }.mapFinIdx fun i a h => f i a ⋯) ++
      { toList := toList✝ }.mapFinIdx fun i a h => f (i + { toList := toList✝¹ }.size) a ⋯

Proof state:
α : Type ?u.52380
β : Type ?u.52470
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
i : Nat
a : α
h : i < K.size
⊢ i < (K ++ L).size

Tactic:
simp

Result:
α : Type ?u.52380
β : Type ?u.52470
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
i : Nat
a : α
h : i < K.size
⊢ i < K.size + L.size

Proof state:
α : Type ?u.52380
β : Type ?u.52470
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
i : Nat
a : α
h : i < L.size
⊢ i + K.size < (K ++ L).size

Tactic:
simp

Result:
α : Type ?u.52380
β : Type ?u.52470
K L : Array α
f : (i : Nat) → α → i < (K ++ L).size → β
i : Nat
a : α
h : i < L.size
⊢ i + K.size < K.size + L.size
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem cotangentEquivIdeal_symm_apply (x : R) (hx : x ∈ I) :
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(R₂ := R)` because `I.toCotangent` suggested `R ⧸ I^2` instead
    I.cotangentEquivIdeal.symm ⟨(I ^ 2).mkQ x,
      -- timeout (200000 heartbeats) without `by exact`
      by exact Submodule.mem_map_of_mem (F := R →ₗ[R] R ⧸ I ^ 2) (f := (I ^ 2).mkQ) hx⟩ =
      I.toCotangent (R := R) ⟨x, hx⟩

Proof state:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩)

Tactic:
ext

Result:
case a.a
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = ↑(I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩))

Proof state:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ I.cotangentEquivIdeal (I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩) =
    I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩)

Tactic:
rw [I.cotangentEquivIdeal.apply_symm_apply]

Result:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩)

Proof state:
case a.a
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = ↑(I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ (Submodule.mkQ (I ^ 2)) x ∈ I.cotangentIdeal

Tactic:
exact Submodule.mem_map_of_mem (F := R →ₗ[R] R ⧸ I ^ 2) (f := (I ^ 2).mkQ) hx

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩

Tactic:
apply I.cotangentEquivIdeal.injective

Result:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ I.cotangentEquivIdeal (I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩) =
    I.cotangentEquivIdeal (I.toCotangent ⟨x, hx⟩)
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_mul_measure_univ (μ : Measure α) [IsFiniteMeasure μ] (f : α → ℝ≥0∞) :
    (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ x, f x ∂μ

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [laverage_eq, ENNReal.div_mul_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
⊢ (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ (x : α), f x ∂μ

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure 0
⊢ (⨍⁻ (a : α), f a ∂0) * 0 univ = ∫⁻ (x : α), f x ∂0

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ (x : α), f x ∂μ

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure 0
⊢ (⨍⁻ (a : α), f a ∂0) * 0 univ = ∫⁻ (x : α), f x ∂0

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma irreducible_polynomial [IsDomain R] : Irreducible W'.polynomial

Proof state:
case intro.intro.intro
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
⊢ 1 < (f + g).degree

Tactic:
rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h

Result:
case intro.intro.intro.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case intro.intro.intro.inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W'.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree
-- Mathlib/Algebra/GradedMonoid.lean
theorem SetLike.coe_list_dProd (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι)
    (fA : ∀ a, A (fι a)) (l : List α) : ↑(@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA)
    = (List.prod (l.map fun a => fA a) : R)

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ ↑((head :: tail).dProd fι fA) = (List.map (fun a => ↑(fA a)) (head :: tail)).prod

Tactic:
rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
  SetLike.coe_list_dProd _ _ _ tail]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
⊢ ↑(l.dProd fι fA) = (List.map (fun a => ↑(fA a)) l).prod

Tactic:
match l with
| [] =>
  rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
| head::tail =>
  rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
    SetLike.coe_list_dProd _ _ _ tail]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
⊢ ↑([].dProd fι fA) = (List.map (fun a => ↑(fA a)) []).prod

Tactic:
rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]

Result:
no goals
-- Mathlib/RingTheory/Smooth/Locus.lean
lemma isOpen_smoothLocus [FinitePresentation R A] : IsOpen (smoothLocus R A)

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : LocalizedModule (Submonoid.powers f) (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.Away f⁄R]
⊢ IsOpen (smoothLocus R Af)

Tactic:
have := LinearEquiv.ofBijective (this.extendScalarsOfIsLocalization
  (.powers f) (Localization.Away f)) this.bijective

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝² : FinitePresentation A (Localization.Away f)
this✝¹ : FinitePresentation R (Localization.Away f)
this✝ : LocalizedModule (Submonoid.powers f) (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.Away f⁄R]
this : LocalizedModule (Submonoid.powers f) (Ω[A⁄R]) ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
⊢ IsOpen (smoothLocus R Af)

Proof state:
case intro.intro.intro.intro.intro.intro
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (⇑(comap (algebraMap A Af)) ⁻¹' smoothLocus R A)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
replace this := (PrimeSpectrum.localization_away_isOpenEmbedding Af f).isOpenMap _ this

Result:
case intro.intro.intro.intro.intro.intro
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (⇑(comap (algebraMap A Af)) '' (⇑(comap (algebraMap A Af)) ⁻¹' smoothLocus R A))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t