harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem dvd_map_of_isScalarTower' (R : Type*) {S : Type*} (K L : Type*) [CommRing R]
    [CommRing S] [Field K] [CommRing L] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L]
    [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S) :
    minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (minpoly R s)

Proof state:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)

Tactic:
apply minpoly.dvd K (algebraMap S L s)

Result:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ (Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0

Proof state:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ (Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0

Tactic:
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]

Result:
case h
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ (algebraMap K L).comp (algebraMap R K) = (algebraMap S L).comp (algebraMap R S)

Proof state:
case h
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ (algebraMap K L).comp (algebraMap R K) = (algebraMap S L).comp (algebraMap R S)

Tactic:
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem fst_prodExtendRight (ab : α₁ × β₁) : (prodExtendRight a e ab).fst = ab.fst

Proof state:
case neg
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ¬ab.1 = a
⊢ ab.1 = ab.1

Tactic:
rfl

Result:
no goals

Proof state:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (if ab.1 = a then (a, e ab.2) else ab).1 = ab.1

Tactic:
split_ifs with h

Result:
case pos
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ab.1 = a
⊢ (a, e ab.2).1 = ab.1

case neg
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ¬ab.1 = a
⊢ ab.1 = ab.1

Proof state:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ ((prodExtendRight a e) ab).1 = ab.1

Tactic:
rw [prodExtendRight]

Result:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ ({ toFun := fun ab => if ab.1 = a then (a, e ab.2) else ab,
          invFun := fun ab => if ab.1 = a then (a, (Equiv.symm e) ab.2) else ab, left_inv := ⋯, right_inv := ⋯ }
        ab).1 =
    ab.1

Proof state:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ ({ toFun := fun ab => if ab.1 = a then (a, e ab.2) else ab,
          invFun := fun ab => if ab.1 = a then (a, (Equiv.symm e) ab.2) else ab, left_inv := ⋯, right_inv := ⋯ }
        ab).1 =
    ab.1

Tactic:
dsimp

Result:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (if ab.1 = a then (a, e ab.2) else ab).1 = ab.1

Proof state:
case pos
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ab.1 = a
⊢ (a, e ab.2).1 = ab.1

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
lemma factorizationLCMLeft_mul_factorizationLCMRight (ha : a ≠ 0) (hb : b ≠ 0) :
    (factorizationLCMLeft a b) * (factorizationLCMRight a b) = lcm a b

Proof state:
case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (fun a_1 b_1 =>
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    fun x1 x2 => x1 ^ x2

Tactic:
ext p n

Result:
case e_g.h.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ((a.lcm b).factorization.prod fun a_1 b_1 =>
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    (a.lcm b).factorization.prod fun x1 x2 => x1 ^ x2

Tactic:
congr

Result:
case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (fun a_1 b_1 =>
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    fun x1 x2 => x1 ^ x2

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

Tactic:
rw [← factorization_prod_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft,
  factorizationLCMRight, ← prod_mul]

Result:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ((a.lcm b).factorization.prod fun a_1 b_1 =>
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    (a.lcm b).factorization.prod fun x1 x2 => x1 ^ x2

Proof state:
case e_g.h.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_bot :
    (⊥ : LieSubmodule R L M).map f = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
M' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f ⊥ = ⊥

Tactic:
ext m

Result:
case h
R : Type u
L : Type v
M : Type w
M' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
m : M'
⊢ m ∈ map f ⊥ ↔ m ∈ ⊥

Proof state:
case h
R : Type u
L : Type v
M : Type w
M' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
m : M'
⊢ m ∈ map f ⊥ ↔ m ∈ ⊥

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) :
    (f * g) • h = f • g • h

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal.sigma fun a => a.1.divisorsAntidiagonal, f x.snd.1 • g x.snd.2 • h x.fst.2 =
    ∑ x ∈ n.divisorsAntidiagonal.sigma fun a => a.2.divisorsAntidiagonal, f x.fst.1 • g x.snd.1 • h x.snd.2

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩)
  (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
⊢ (f * g) • h = f • g • h

Tactic:
ext n

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ((f * g) • h) n = (f • g • h) n

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ((f * g) • h) n = (f • g • h) n

Tactic:
simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, Finset.sum_sigma']

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal.sigma fun a => a.1.divisorsAntidiagonal, f x.snd.1 • g x.snd.2 • h x.fst.2 =
    ∑ x ∈ n.divisorsAntidiagonal.sigma fun a => a.2.divisorsAntidiagonal, f x.fst.1 • g x.snd.1 • h x.snd.2
-- Mathlib/ModelTheory/Satisfiability.lean
theorem realize_sentence_iff (h : T.IsComplete) (φ : L.Sentence) (M : Type*) [L.Structure M]
    [M ⊨ T] [Nonempty M] : M ⊨ φ ↔ T ⊨ᵇ φ

Proof state:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
rcases h.2 φ with hφ | hφn

Result:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Proof state:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
exact
  iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M))
    ((h.models_not_iff φ).1 hφn)

Result:
no goals

Proof state:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
exact iff_of_true (hφ.realize_sentence M) hφ

Result:
no goals
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem Sum.dist_eq_glueDist {p q : X ⊕ Y} (x : X) (y : Y) :
    Sum.dist p q =
      glueDist (fun _ : Unit => Nonempty.some ⟨x⟩) (fun _ : Unit => Nonempty.some ⟨y⟩) 1 p q

Proof state:
case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => ⋯.some) (fun x => ⋯.some) 1 (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [Sum.dist, glueDist, dist_comm, add_comm,
add_left_comm, add_assoc]

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
⊢ Sum.dist p q = glueDist (fun x_1 => ⋯.some) (fun x => ⋯.some) 1 p q

Tactic:
cases p <;> cases q <;> first |rfl|simp [Sum.dist, glueDist, dist_comm, add_comm,
  add_left_comm, add_assoc]

Result:
no goals

Proof state:
case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => ⋯.some) (fun x => ⋯.some) 1 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem equiv_zero_of_val_eq_of_equiv_zero {f g : PadicSeq p}
    (h : ∀ k, padicNorm p (f k) = padicNorm p (g k)) (hf : f ≈ 0) : g ≈ 0 := fun ε hε ↦
  let ⟨i, hi⟩ := hf _ hε
  ⟨i, fun j hj ↦ by simpa [h] using hi _ hj⟩

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
ε : ℚ
hε : ε > 0
i : ℕ
hi : ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε
j : ℕ
hj : j ≥ i
⊢ padicNorm p (↑(g - 0) j) < ε

Tactic:
simpa [h] using hi _ hj

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_empty_list_of_contains_eq_false [LawfulBEq α]
    {l : List ((a : α) × β a)} {k : α} {fallback : β k}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (insertMany empty l).1.getD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
fallback : β k
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ empty.getD k fallback = fallback

Tactic:
apply getD_empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
fallback : β k
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (empty.insertMany l).val.getD k fallback = fallback

Tactic:
rw [getD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ contains_eq_false]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
fallback : β k
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ empty.getD k fallback = fallback
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem coe_mem_principalUnitGroup_iff {x : A.unitGroup} :
    (x : Kˣ) ∈ A.principalUnitGroup ↔
      A.unitGroupMulEquiv x ∈ (Units.map (IsLocalRing.residue A).toMonoidHom).ker

Proof state:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π ↑(A.unitGroupMulEquiv x) = 1

Tactic:
rw [← π.map_one, ← sub_eq_zero, ← π.map_sub, Ideal.Quotient.eq_zero_iff_mem, valuation_lt_one_iff]

Result:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ A.valuation ↑(↑(A.unitGroupMulEquiv x) - 1) < 1

Proof state:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ A.valuation ↑(↑(A.unitGroupMulEquiv x) - 1) < 1

Tactic:
simp [mem_principalUnitGroup_iff]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1

Tactic:
convert_to _ ↔ π _ = 1

Result:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π ↑(A.unitGroupMulEquiv x) = 1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ ↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker

Tactic:
rw [MonoidHom.mem_ker, Units.ext_iff]

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1

Tactic:
let π := Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1
-- Mathlib/RingTheory/Ideal/Height.lean
lemma Ideal.primeHeight_ne_top (I : Ideal R) [I.FiniteHeight] [h : I.IsPrime] :
    I.primeHeight ≠ ⊤

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.FiniteHeight
h : I.IsPrime
⊢ I.height ≠ ⊤

Tactic:
exact Ideal.height_ne_top h.ne_top

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.FiniteHeight
h : I.IsPrime
⊢ I.primeHeight ≠ ⊤

Tactic:
rw [← I.height_eq_primeHeight]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.FiniteHeight
h : I.IsPrime
⊢ I.height ≠ ⊤
-- Mathlib/Analysis/Convex/Side.lean
theorem wSameSide_smul_vsub_vadd_left {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) {t : R} (ht : 0 ≤ t) : s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)

Tactic:
exact SameRay.sameRay_nonneg_smul_left _ ht

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)

Tactic:
rw [vadd_vsub]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_left' (a b : α) : toIcoMod hp (p + a) b = p + toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_right', add_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem image_gaugeRescaleHomeomorph_closure {s t : Set E}
    (hsc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) (hsb : IsVonNBounded ℝ s)
    (htc : Convex ℝ t) (ht₀ : t ∈ 𝓝 0) (htb : IsVonNBounded ℝ t) :
    gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb '' closure s = closure t

Proof state:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ closure t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s

Tactic:
rw [← Homeomorph.preimage_symm, ← image_subset_iff]

Result:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' closure t ⊆ closure s

Proof state:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s = closure t

Tactic:
refine Subset.antisymm (mapsTo_gaugeRescale_closure hsc hs₀ htc
  (mem_of_mem_nhds ht₀) (absorbent_nhds_zero ht₀)).image_subset ?_

Result:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ closure t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s

Proof state:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' closure t ⊆ closure s

Tactic:
exact (mapsTo_gaugeRescale_closure htc ht₀ hsc
  (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀)).image_subset

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
/-- If `m : M → N` is a subadditive function (`m (a + b) ≤ m a + m b`) and `s` is a nonempty set,
then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
lemma le_expect_nonempty_of_subadditive (m : M → N) (h_mul : ∀ a b, m (a + b) ≤ m a + m b)
    (h_div : ∀ (n : ℕ) a, m (a /ℚ n) = m a /ℚ n) (hs : s.Nonempty) :
    m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) :=
  le_expect_nonempty_of_subadditive_on_pred (p := fun _ ↦ True) (by simpa) (by simp) (by simpa) hs
    (by simp)

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (a b : M), (fun x => True) a → (fun x => True) b → (fun x => True) (a + b)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ i ∈ s, (fun x => True) (f i)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (a b : M), (fun x => True) a → (fun x => True) b → m (a + b) ≤ m a + m b

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (n : ℕ) (a : M), (fun x => True) a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a

Tactic:
simpa

Result:
no goals