harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Map.lean
theorem comap_inf_principal_range : comap m (g ⊓ 𝓟 (range m)) = comap m g

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
⊢ comap m (g ⊓ 𝓟 (range m)) = comap m g

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
lemma epi_f₃₄ [Epi sq.f₁₂] : Epi sq.f₃₄

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.f₁₂

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
this : Epi sq.flip.f₁₃
⊢ Epi sq.f₃₄

Tactic:
exact h.flip.epi_f₂₄

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.flip.f₁₃

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.f₁₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
⊢ Epi sq.f₃₄

Tactic:
have : Epi sq.flip.f₁₃ := by dsimp; infer_instance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₂
this : Epi sq.flip.f₁₃
⊢ Epi sq.f₃₄
-- Mathlib/FieldTheory/KummerExtension.lean
lemma adjoinRootXPowSubCEquiv_root :
    adjoinRootXPowSubCEquiv hζ H hα (root _) = α

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a)) = α

Tactic:
rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftHom_root]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_eq_iff_multiplicity_eq_of_ne_one {n : ℕ} (h : n ≠ 1) :
    emultiplicity a b = n ↔ multiplicity a b = n

Proof state:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
h₂ : multiplicity a b = n
⊢ emultiplicity a b = ↑n

Tactic:
simpa [multiplicity, WithTop.untopD_eq_iff, h] using h₂

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n → multiplicity a b = n

Tactic:
exact multiplicity_eq_of_emultiplicity_eq_some

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n ↔ multiplicity a b = n

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n → multiplicity a b = n

case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n

Proof state:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n

Tactic:
intro h₂

Result:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
h₂ : multiplicity a b = n
⊢ emultiplicity a b = ↑n
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_zero : ContDiff 𝕜 0 f ↔ Continuous f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 0 f ↔ Continuous f

Tactic:
rw [← contDiffOn_univ, continuous_iff_continuousOn_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ

Tactic:
exact contDiffOn_zero

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem isPrime_ideal_prod_top' {I : Ideal S} [h : I.IsPrime] : (prod (⊤ : Ideal R) I).IsPrime

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : I.IsPrime
this : (I.prod ⊤).IsPrime := isPrime_ideal_prod_top
⊢ (map (↑RingEquiv.prodComm) (I.prod ⊤)).IsPrime

Tactic:
exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : I.IsPrime
⊢ (⊤.prod I).IsPrime

Tactic:
letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : I.IsPrime
this : (I.prod ⊤).IsPrime := isPrime_ideal_prod_top
⊢ (⊤.prod I).IsPrime

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : I.IsPrime
this : (I.prod ⊤).IsPrime := isPrime_ideal_prod_top
⊢ (⊤.prod I).IsPrime

Tactic:
rw [← map_prodComm_prod]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : I.IsPrime
this : (I.prod ⊤).IsPrime := isPrime_ideal_prod_top
⊢ (map (↑RingEquiv.prodComm) (I.prod ⊤)).IsPrime
-- Mathlib/GroupTheory/Perm/DomMulAct.lean
lemma mem_stabilizer_iff {g : (Perm α)ᵈᵐᵃ} :
    g ∈ stabilizer (Perm α)ᵈᵐᵃ f ↔ f ∘ (mk.symm g :) = f

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g • f = f ↔ f ∘ ⇑(mk.symm g) = f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g ∈ stabilizer (Perm α)ᵈᵐᵃ f ↔ f ∘ ⇑(mk.symm g) = f

Tactic:
simp only [MulAction.mem_stabilizer_iff]

Result:
α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g • f = f ↔ f ∘ ⇑(mk.symm g) = f
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem map_T (f : R →+* R') (n : ℤ) : map f (T R n) = T R' n

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (T R n) = T R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
    ih1, ih2]
| neg_add_one n ih1 ih2 =>
  simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
    ih2]

Result:
no goals

Proof state:
case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (T R 0) = T R' 0

Tactic:
simp

Result:
no goals

Proof state:
case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (T R 1) = T R' 1

Tactic:
simp

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-↑n)) = T R' (-↑n)
ih2 : map f (T R (-↑n + 1)) = T R' (-↑n + 1)
⊢ map f (T R (-↑n - 1)) = T R' (-↑n - 1)

Tactic:
simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
  ih2]

Result:
no goals

Proof state:
case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (↑n + 1)) = T R' (↑n + 1)
ih2 : map f (T R ↑n) = T R' ↑n
⊢ map f (T R (↑n + 2)) = T R' (↑n + 2)

Tactic:
simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
  ih1, ih2]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem max_def' [LinearOrder α] (a b : α) : max a b = if b ≤ a then a else b

Proof state:
case inr.inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Tactic:
rw [if_pos eq.le, if_pos eq.ge, eq]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Tactic:
rcases lt_trichotomy a b with (lt | eq | gt)

Result:
case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

case inr.inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

case inr.inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Proof state:
case inr.inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Tactic:
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ a ⊔ b = if b ≤ a then a else b

Tactic:
rw [max_def]

Result:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b

Tactic:
rw [if_pos lt.le, if_neg (not_le.mpr lt)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem mem_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) (f : A) :
    f ∈ vanishingIdeal t ↔ ∀ x : ProjectiveSpectrum 𝒜, x ∈ t → f ∈ x.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal

Tactic:
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/MulAction.lean
theorem norm_smul_le (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
simpa [smul_zero] using dist_smul_pair r 0 x

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_preΨ'_pos {n : ℕ} (hn : 2 < n) (h : (n : R) ≠ 0) : 0 < (W.preΨ' n).natDegree

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 0 < (W.preΨ' n).natDegree

Tactic:
simp only [W.natDegree_preΨ' h, Nat.div_pos_iff, zero_lt_two, true_and]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 2 ≤ n ^ 2 - if Even n then 4 else 1

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < n
h : ↑n ≠ 0
⊢ 2 ≤ n ^ 2 - if Even n then 4 else 1

Tactic:
split_ifs <;>
  exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_of_le_left hn 2) _

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem finrank_eq_one_iff_of_nonzero' (v : V) (nz : v ≠ 0) :
    finrank K V = 1 ↔ ∀ w : V, ∃ c : K, c • v = w

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ span K {v} = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w

Tactic:
apply span_singleton_eq_top_iff

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w

Tactic:
rw [finrank_eq_one_iff_of_nonzero v nz]

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ span K {v} = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w
-- Mathlib/Order/RelSeries.lean
@[simp]
lemma last_drop (p : RelSeries r) (i : Fin (p.length + 1)) : (p.drop i).last = p.last

Proof state:
case e_a.e_val
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ p.length - ↑i + ↑i = p.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).last = p.last

Tactic:
simp only [last, drop, Fin.last]

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ p.toFun ⟨p.length - ↑i + ↑i, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ p.toFun ⟨p.length - ↑i + ↑i, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩

Tactic:
congr

Result:
case e_a.e_val
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ p.length - ↑i + ↑i = p.length
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_prime_pow [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ℕ) :
    factors (p ^ k) = WithTop.some (Multiset.replicate k ⟨p, hp⟩) :=
  eq_of_prod_eq_prod
    (by
      rw [Associates.factors_prod, FactorSet.prod.eq_def]
      dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k =
    match ↑(replicate k ⟨p, hp⟩) with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod

Tactic:
dsimp

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = (Multiset.map Subtype.val (replicate k ⟨p, hp⟩)).prod

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ (p ^ k).factors.prod = FactorSet.prod ↑(replicate k ⟨p, hp⟩)

Tactic:
rw [Associates.factors_prod, FactorSet.prod.eq_def]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k =
    match ↑(replicate k ⟨p, hp⟩) with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = (Multiset.map Subtype.val (replicate k ⟨p, hp⟩)).prod

Tactic:
rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem subtypePerm_zpow (f : Perm α) (n : ℤ) (hf) :
    (f.subtypePerm hf ^ n : Perm { x // p x }) = (f ^ n).subtypePerm (zpow_aux hf)

Proof state:
α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p x ↔ p (f x)
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
cases n with
| ofNat n => exact subtypePerm_pow _ _ _
| negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

Result:
no goals

Proof state:
case negSucc
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
n : ℕ
⊢ f.subtypePerm hf ^ Int.negSucc n = (f ^ Int.negSucc n).subtypePerm ⋯

Tactic:
simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

Result:
no goals

Proof state:
case ofNat
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
n : ℕ
⊢ f.subtypePerm hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm ⋯

Tactic:
exact subtypePerm_pow _ _ _

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive]
lemma map_comp_mul_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) :
    f ∘ (g * h⁻¹) = f ∘ g * (f ∘ h)⁻¹

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
⊢ ⇑f ∘ (g * h⁻¹) = ⇑f ∘ g * (⇑f ∘ h)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_single_ne_zero (a : A) {r : R} (hr : r ≠ 0) :
    (single a r).supDegree D = D a

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : r ≠ 0
⊢ supDegree D (single a r) = D a

Tactic:
rw [supDegree, Finsupp.support_single_ne_zero a hr, Finset.sup_singleton]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated
by `star s * s` for `s : R`. -/
lemma of_nonneg_iff [NonUnitalRing R] [PartialOrder R] [StarRing R]
    (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
    (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)) :
    StarOrderedRing R where
  le_iff x y

Proof state:
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (range fun s => star s * s)
x y : R
this : AddLeftMono R
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

Tactic:
simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)

Result:
no goals

Proof state:
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (range fun s => star s * s)
x y : R
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p

Tactic:
have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩

Result:
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (range fun s => star s * s)
x y : R
this : AddLeftMono R
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem equiv {C : Type*} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension S A B]
    (f : B ≃ₐ[A] C) : IsCyclotomicExtension S A C

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝¹ : Algebra B C := (↑f).toAlgebra
this✝ : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C

Tactic:
exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)

Result:
no goals

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
⊢ IsCyclotomicExtension S A C

Tactic:
letI : Algebra B C := f.toAlgHom.toRingHom.toAlgebra

Result:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this : Algebra B C := (↑f).toAlgebra
⊢ IsCyclotomicExtension S A C

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝ : Algebra B C := (↑f).toAlgebra
this : IsCyclotomicExtension {1} B C
⊢ IsCyclotomicExtension S A C

Tactic:
haveI : IsScalarTower A B C := IsScalarTower.of_algHom f.toAlgHom

Result:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝¹ : Algebra B C := (↑f).toAlgebra
this✝ : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this : Algebra B C := (↑f).toAlgebra
⊢ IsCyclotomicExtension S A C

Tactic:
haveI : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective

Result:
S : Set ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝ : Algebra B C := (↑f).toAlgebra
this : IsCyclotomicExtension {1} B C
⊢ IsCyclotomicExtension S A C
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem FinitePlace.norm_lt_one_iff_mem (x : 𝓞 (WithVal (v.valuation K))) :
    ‖embedding v x‖ < 1 ↔ x ∈ v.asIdeal

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ ‖(embedding v) ↑x‖ < 1 ↔ x ∈ v.asIdeal

Tactic:
erw [norm_def_int, NNReal.coe_lt_one, toNNReal_lt_one_iff (one_lt_absNorm_nnreal v),
  intValuation_lt_one_iff_dvd]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ v.asIdeal ∣ span {x} ↔ x ∈ v.asIdeal

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ v.asIdeal ∣ span {x} ↔ x ∈ v.asIdeal

Tactic:
exact dvd_span_singleton

Result:
no goals
-- Mathlib/Order/Fin/Basic.lean
lemma predAbove_left_monotone (i : Fin (n + 1)) : Monotone fun p ↦ predAbove p i := fun a b H ↦ by
  dsimp [predAbove]
  split_ifs with ha hb hb
  · rfl
  · exact pred_le _
  · have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
    exact absurd H this.not_le
  · rfl

Proof state:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
this : b < a
⊢ i.castPred ⋯ ≤ i.pred ⋯

Tactic:
exact absurd H this.not_le

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯) ≤ if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯

Tactic:
split_ifs with ha hb hb

Result:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯

case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Proof state:
case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

Tactic:
have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))

Result:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
this : b < a
⊢ i.castPred ⋯ ≤ i.pred ⋯

Proof state:
case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

Tactic:
exact pred_le _

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (fun p => p.predAbove i) a ≤ (fun p => p.predAbove i) b

Tactic:
dsimp [predAbove]

Result:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯) ≤ if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem zeroRootSubalgebra_eq_iff_is_cartan [IsNoetherian R L] :
    zeroRootSubalgebra R L H = H ↔ H.IsCartanSubalgebra :=
  ⟨is_cartan_of_zeroRootSubalgebra_eq R L H, by intros; simp⟩

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : LieRing.IsNilpotent ↥H
inst✝ : IsNoetherian R L
⊢ H.IsCartanSubalgebra → zeroRootSubalgebra R L H = H

Tactic:
intros

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : LieRing.IsNilpotent ↥H
inst✝ : IsNoetherian R L
a✝ : H.IsCartanSubalgebra
⊢ zeroRootSubalgebra R L H = H

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : LieRing.IsNilpotent ↥H
inst✝ : IsNoetherian R L
a✝ : H.IsCartanSubalgebra
⊢ zeroRootSubalgebra R L H = H

Tactic:
simp

Result:
no goals