harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/GoingUp.lean
lemma primesOver_bot [Nontrivial A] [IsDomain B] : primesOver (⊥ : Ideal A) B = {⊥}

Proof state:
case h
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
p : Ideal B
⊢ p ∈ {⊥} → p ∈ ⊥.primesOver B

Tactic:
rintro rfl

Result:
case h
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
⊢ ⊥ ∈ ⊥.primesOver B

Proof state:
case h
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
p : Ideal B
⊢ p ∈ ⊥.primesOver B ↔ p ∈ {⊥}

Tactic:
refine ⟨fun ⟨_, ⟨h⟩⟩ ↦ p.eq_bot_of_comap_eq_bot h.symm, ?_⟩

Result:
case h
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
p : Ideal B
⊢ p ∈ {⊥} → p ∈ ⊥.primesOver B

Proof state:
case h
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
⊢ ⊥ ∈ ⊥.primesOver B

Tactic:
exact ⟨Ideal.bot_prime, Ideal.bot_liesOver_bot A B⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
⊢ ⊥.primesOver B = {⊥}

Tactic:
ext p

Result:
case h
A : Type u_1
inst✝⁶ : CommRing A
B : Type u_2
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Nontrivial A
inst✝ : IsDomain B
p : Ideal B
⊢ p ∈ ⊥.primesOver B ↔ p ∈ {⊥}
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.injOn_iff_bijOn_of_mapsTo (hs : s.Finite) (hm : MapsTo f s s) :
    InjOn f s ↔ BijOn f s s

Proof state:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ InjOn f s ↔ BijOn f s s

Tactic:
refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩

Result:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
⊢ SurjOn f s s

Proof state:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
this : Finite ↑s
⊢ SurjOn f s s

Tactic:
exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

Result:
no goals

Proof state:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
⊢ SurjOn f s s

Tactic:
have : Finite s := finite_coe_iff.mpr hs

Result:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
this : Finite ↑s
⊢ SurjOn f s s
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma boundaryGE {i' : ι'} {j : ι} (hj : c'.Rel i' (e.f j)) (hi' : ∀ i, e.f i ≠ i') :
    e.BoundaryGE j

Proof state:
case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ c'.Rel (c'.prev (e.f j)) (e.f j)

Tactic:
simpa only [c'.prev_eq' hj] using hj

Result:
no goals

Proof state:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ e.f i = i'

Tactic:
rw [← c'.prev_eq' hj, c'.prev_eq' hi]

Result:
no goals

Proof state:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False

Tactic:
apply hi' i

Result:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ e.f i = i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ e.BoundaryGE j

Tactic:
constructor

Result:
case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ c'.Rel (c'.prev (e.f j)) (e.f j)

case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)

Proof state:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)

Tactic:
intro i hi

Result:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_comp : natDegree (p.comp q) = natDegree p * natDegree q

Proof state:
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases q0 : q.natDegree = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
  ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases p0 : p = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
simp only [p0, zero_comp, natDegree_zero, zero_mul]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
  natDegree_C, mul_zero]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem support_mul_subset_add_support [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} :
    support (x * y) ⊆ support x + support y

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).support ⊆ x.support +ᵥ y.support

Tactic:
exact HahnModule.support_smul_subset_vadd_support

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ (x * y).support ⊆ x.support + y.support

Tactic:
rw [← of_symm_smul_of_eq_mul, ← vadd_eq_add]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).support ⊆ x.support +ᵥ y.support
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem BEqCmp.compareOfLessAndEq
    [LT α] [DecidableRel (LT.lt (α := α))] [DecidableEq α] [BEq α] [LawfulBEq α]
    (lt_irrefl : ∀ x : α, ¬x < x) :
    BEqCmp (α := α) (compareOfLessAndEq · ·) where
  cmp_iff_beq {x y}

Proof state:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x y : α
⊢ compareOfLessAndEq x y = Ordering.eq ↔ (x == y) = true

Tactic:
simp [compareOfLessAndEq]

Result:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x y : α
⊢ (if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt) = Ordering.eq ↔ x = y

Proof state:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x : α
h✝ : x < x
⊢ False

Tactic:
exact lt_irrefl _ ‹_›

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x y : α
⊢ (if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt) = Ordering.eq ↔ x = y

Tactic:
split <;> [skip; split] <;> simp [*]

Result:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x y : α
h✝ : x < y
⊢ ¬x = y

Proof state:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x y : α
h✝ : x < y
⊢ ¬x = y

Tactic:
rintro rfl

Result:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel LT.lt
inst✝² : DecidableEq α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
lt_irrefl : ∀ (x : α), ¬x < x
x : α
h✝ : x < x
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : x ≤ y) (h₂ : 0 ≤ z) : x ^ z ≤ y ^ z

Proof state:
case inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z

Tactic:
rcases eq_or_lt_of_le h₂ with (rfl | h₂')

Result:
case inr.inl
x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

case inr.inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z

Proof state:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
⊢ x ^ z ≤ y ^ z

Tactic:
rcases eq_or_lt_of_le h₁ with (rfl | h₁')

Result:
case inl
x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z

case inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z

Proof state:
case inr.inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z

Tactic:
exact le_of_lt (rpow_lt_rpow h h₁' h₂')

Result:
no goals

Proof state:
case inl
x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z

Tactic:
rfl

Result:
no goals

Proof state:
case inr.inl
x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₄_of_isCharTwoJNeZeroNF : W.b₄ = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 2 * 0 + W.a₁ * 0 = 0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₄ = 0

Tactic:
rw [b₄, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 2 * 0 + W.a₁ * 0 = 0
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma le_stabilizer_smul_left [SMul α β] [IsScalarTower G α β] (a : α) (b : β) :
    stabilizer G a ≤ stabilizer G (a • b)

Proof state:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b

Tactic:
rintro a h

Result:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
a : G
h : a • a✝ = a✝
⊢ (a • a✝) • b = a✝ • b

Proof state:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
a : G
h : a • a✝ = a✝
⊢ (a • a✝) • b = a✝ • b

Tactic:
rw [h]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ stabilizer G a ≤ stabilizer G (a • b)

Tactic:
simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]

Result:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_div_dvd (p q : K[X]) : denom (algebraMap _ _ p / algebraMap _ _ q) ∣ q

Proof state:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0

Tactic:
simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

Result:
no goals

Proof state:
case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q

Tactic:
simp [hq]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q

Tactic:
by_cases hq : q = 0

Result:
case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q

case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q

Proof state:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ q / gcd p q ∣ q

Tactic:
exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q

Tactic:
rw [denom_div _ hq, C_mul_dvd]

Result:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ q / gcd p q ∣ q

case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
/-- If `B` is a faithfully flat `A`-algebra, the preimage of the pushforward of any
ideal `I` is again `I`. -/
lemma Ideal.comap_map_eq_self_of_faithfullyFlat (I : Ideal A) :
    (I.map (algebraMap A B)).comap (algebraMap A B) = I

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
⊢ (Quotient.mk I) x = 0

Tactic:
apply inj

Result:
case a
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
⊢ (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) =
    (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) 0
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_inner_right (A : E →ₗ[𝕜] F) (x : E) (y : F) : ⟪x, adjoint A y⟫ = ⟪A x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, ↑(ContinuousLinearMap.adjoint (toContinuousLinearMap ↑(toContinuousLinearMap A))) y⟫_𝕜 =
    ⟪↑(toContinuousLinearMap A) x, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
⊢ ⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
haveI := FiniteDimensional.complete 𝕜 E

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this : CompleteSpace E
⊢ ⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this : CompleteSpace E
⊢ ⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
haveI := FiniteDimensional.complete 𝕜 F

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, ↑(ContinuousLinearMap.adjoint (toContinuousLinearMap ↑(toContinuousLinearMap A))) y⟫_𝕜 =
    ⟪↑(toContinuousLinearMap A) x, y⟫_𝕜

Tactic:
exact ContinuousLinearMap.adjoint_inner_right _ x y

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem IsSimpleModule.nontrivial [IsSimpleModule R M] : Nontrivial M :=
  ⟨⟨0, by
      have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
      contrapose! h
      ext x
      simp [Submodule.mem_bot, Submodule.mem_top, h x]⟩⟩

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y

Tactic:
contrapose! h

Result:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
⊢ ∃ y, 0 ≠ y

Tactic:
have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top

Result:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤

Tactic:
ext x

Result:
case h
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
x : M
⊢ x ∈ ⊥ ↔ x ∈ ⊤

Proof state:
case h
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
x : M
⊢ x ∈ ⊥ ↔ x ∈ ⊤

Tactic:
simp [Submodule.mem_bot, Submodule.mem_top, h x]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem abelian_derivedAbelianOfIdeal (I : LieIdeal R L) :
    IsLieAbelian (derivedAbelianOfIdeal I)

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = k + 1
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
rw [derivedSeries_of_derivedLength_succ] at h

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥(derivedAbelianOfIdeal I)

Tactic:
dsimp only [derivedAbelianOfIdeal]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian
    ↥(match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = 0
⊢ IsLieAbelian ↥⊥

Tactic:
infer_instance

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = 0
⊢ IsLieAbelian
    ↥(match 0 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
dsimp

Result:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = 0
⊢ IsLieAbelian ↥⊥

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
exact h.1

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian
    ↥(match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
rcases h : derivedLengthOfIdeal R L I with - | k

Result:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : derivedLengthOfIdeal R L I = 0
⊢ IsLieAbelian
    ↥(match 0 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = k + 1
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc_C_mul (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) :
    trunc R n (C σ R a * p) = MvPolynomial.C a * trunc R n p

Proof state:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) ((C σ R) a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc R n) p)

Tactic:
simp [coeff_trunc]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc R n) ((C σ R) a * p) = MvPolynomial.C a * (trunc R n) p

Tactic:
ext m

Result:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) ((C σ R) a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc R n) p)