harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Defs.lean
theorem map_zero [Zero α] [Zero β] (f : α → β) (h : f 0 = 0) :
    (0 : Matrix m n α).map f = 0

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝

Tactic:
simp [h]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
⊢ map 0 f = 0

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝
-- Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
theorem LocalizationMap.subsingleton (f : Submonoid.LocalizationMap S N) (h : 0 ∈ S) :
    Subsingleton N

Proof state:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
⊢ Subsingleton N

Tactic:
refine ⟨fun a b ↦ ?_⟩

Result:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ a = b

Proof state:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ ↑⟨0, h⟩ * (↑(f.sec b).2 * (f.sec a).1) = ↑⟨0, h⟩ * (↑(f.sec a).2 * (f.sec b).1)

Tactic:
simp only [zero_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ ∃ c, ↑c * (↑(f.sec b).2 * (f.sec a).1) = ↑c * (↑(f.sec a).2 * (f.sec b).1)

Tactic:
exact ⟨⟨0, h⟩, by simp only [zero_mul]⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ a = b

Tactic:
rw [← LocalizationMap.mk'_sec f a, ← LocalizationMap.mk'_sec f b, LocalizationMap.eq]

Result:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ ∃ c, ↑c * (↑(f.sec b).2 * (f.sec a).1) = ↑c * (↑(f.sec a).2 * (f.sec b).1)
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem zoom_fill' (cut : α → Ordering) (t : RBNode α) (path : Path α) :
    fill' (zoom cut t path) = path.fill t

Proof state:
α : Type u_1
cut : α → Ordering
t : RBNode α
path : Path α
⊢ fill' (zoom cut t path) = path.fill t

Tactic:
induction t generalizing path with
| nil => rfl
| node _ _ _ _ iha ihb => unfold zoom; split <;> [apply iha; apply ihb; rfl]

Result:
no goals

Proof state:
case nil
α : Type u_1
cut : α → Ordering
path : Path α
⊢ fill' (zoom cut nil path) = path.fill nil

Tactic:
rfl

Result:
no goals

Proof state:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
iha : ∀ (path : Path α), fill' (zoom cut l✝ path) = path.fill l✝
ihb : ∀ (path : Path α), fill' (zoom cut r✝ path) = path.fill r✝
path : Path α
⊢ fill' (zoom cut (node c✝ l✝ v✝ r✝) path) = path.fill (node c✝ l✝ v✝ r✝)

Tactic:
unfold zoom

Result:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
iha : ∀ (path : Path α), fill' (zoom cut l✝ path) = path.fill l✝
ihb : ∀ (path : Path α), fill' (zoom cut r✝ path) = path.fill r✝
path : Path α
⊢ fill'
      (match cut v✝ with
      | Ordering.lt => zoom cut l✝ (left c✝ path v✝ r✝)
      | Ordering.gt => zoom cut r✝ (right c✝ l✝ v✝ path)
      | Ordering.eq => (node c✝ l✝ v✝ r✝, path)) =
    path.fill (node c✝ l✝ v✝ r✝)

Proof state:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
iha : ∀ (path : Path α), fill' (zoom cut l✝ path) = path.fill l✝
ihb : ∀ (path : Path α), fill' (zoom cut r✝ path) = path.fill r✝
path : Path α
⊢ fill'
      (match cut v✝ with
      | Ordering.lt => zoom cut l✝ (left c✝ path v✝ r✝)
      | Ordering.gt => zoom cut r✝ (right c✝ l✝ v✝ path)
      | Ordering.eq => (node c✝ l✝ v✝ r✝, path)) =
    path.fill (node c✝ l✝ v✝ r✝)

Tactic:
split <;> [apply iha; apply ihb; rfl]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem singleton_zero_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) :
    IsCyclotomicExtension ∅ A B

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
x : B
hx : x ∈ ⊤
⊢ x ∈ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1}

Tactic:
rw [← h] at hx

Result:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
x : B
hx : x ∈ ⊥
⊢ x ∈ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1}

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
x : B
hx : x ∈ ⊥
⊢ x ∈ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1}

Tactic:
simpa using hx

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
⊢ IsCyclotomicExtension ∅ A B

Tactic:
refine (iff_adjoin_eq_top _ A _).2
  ⟨fun s hs => by simp at hs, _root_.eq_top_iff.2 fun x hx => ?_⟩

Result:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
x : B
hx : x ∈ ⊤
⊢ x ∈ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1}

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
s : ℕ+
hs : s ∈ ∅
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
simp at hs

Result:
no goals
-- Mathlib/Logic/Encodable/Basic.lean
theorem Subtype.encode_eq (a : Subtype P) : encode a = encode a.val

Proof state:
case mk
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode ⟨val✝, property✝⟩ = encode ↑⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
⊢ encode a = encode ↑a

Tactic:
cases a

Result:
case mk
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode ⟨val✝, property✝⟩ = encode ↑⟨val✝, property✝⟩
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem neg_add_cancel {X Y : C} (a : X ⟶ Y) : -a + a = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ -a + a = 0

Tactic:
rw [add_comm, add_neg_cancel]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem eq_neg_one_iff' {a : ℕ} : legendreSym p a = -1 ↔ ¬IsSquare (a : ZMod p)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a

Tactic:
rw [eq_neg_one_iff]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare ↑↑a ↔ ¬IsSquare ↑a

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare ↑↑a ↔ ¬IsSquare ↑a

Tactic:
norm_cast

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_smul (P : Fin 3 → F) {u : F} (hu : IsUnit u) :
    toAffine W (u • P) = toAffine W P

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z ^ 2 = P x / P z ^ 2 ∧ (u • P) y / (u • P) z ^ 3 = P y / P z ^ 3

Tactic:
simp only [smul_fin3_ext, mul_pow, mul_div_mul_left _ _ (hu.pow _).ne_zero, and_self]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
  toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]

Result:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z ^ 2 = P x / P z ^ 2 ∧ (u • P) y / (u • P) z ^ 3 = P y / P z ^ 3

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hP : W.Nonsingular P

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem mul_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff σ R φ = u) :
    φ * invOfUnit φ u = 1 :=
  ext fun n =>
    letI := Classical.decEq (σ →₀ ℕ)
    if H : n = 0 then by
      rw [H]
      simp [coeff_mul, support_single_ne_zero, h]
    else by
      classical
      have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n

Proof state:
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ∈ (antidiagonal n).erase (0, n)
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, n).2 then (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) else 0

Tactic:
rw [Finset.mem_erase, mem_antidiagonal] at hij

Result:
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = n
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, n).2 then (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) else 0
-- Mathlib/NumberTheory/ADEInequality.lean
theorem lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < sumInv {2, q, r}) : q < 4

Proof state:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ q < 4

Tactic:
have h4 : (0 : ℚ) < 4 := by norm_num

Result:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
h4 : 0 < 4
⊢ q < 4

Proof state:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
h4 : 0 < 4
⊢ q < 4

Tactic:
contrapose! H

Result:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1

Tactic:
calc
  (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
  _ = 1 := by norm_num

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ (↑↑r)⁻¹ ≤ 4⁻¹

Tactic:
rw [inv_le_inv₀ _ h4]

Result:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 4 ≤ ↑↑r

q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < ↑↑r

Tactic:
norm_num

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1

Tactic:
have h4r := H.trans hqr

Result:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 4 ≤ ↑↑r

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ 2⁻¹ + 4⁻¹ + 4⁻¹ = 1

Tactic:
norm_num

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 0 < ↑↑q

Tactic:
norm_num

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ (↑↑q)⁻¹ ≤ 4⁻¹

Tactic:
rw [inv_le_inv₀ _ h4]

Result:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 4 ≤ ↑↑q

q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 0 < ↑↑q

Proof state:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ 0 < 4

Tactic:
norm_num

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 4 ≤ ↑↑q

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1

Tactic:
rw [sumInv_pqr]

Result:
q r : ℕ+
hqr : q ≤ r
h4 : 0 < 4
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
-- Mathlib/RingTheory/Localization/Defs.lean
theorem isDomain_of_le_nonZeroDivisors [Algebra A S] {M : Submonoid A} [IsLocalization M S]
    (hM : M ≤ nonZeroDivisors A) : IsDomain S

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
⊢ NoZeroDivisors S

Tactic:
exact noZeroDivisors_of_le_nonZeroDivisors _ hM

Result:
no goals

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
⊢ Nontrivial S

Tactic:
exact
  ⟨⟨(algebraMap A S) 0, (algebraMap A S) 1, fun h =>
      zero_ne_one (IsLocalization.injective S hM h)⟩⟩

Result:
no goals

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
⊢ IsDomain S

Tactic:
apply @NoZeroDivisors.to_isDomain _ _ (id _) (id _)

Result:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
⊢ Nontrivial S

S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
⊢ NoZeroDivisors S
-- Mathlib/RingTheory/Ideal/Colon.lean
theorem _root_.Ideal.annihilator_quotient {I : Ideal R} [I.IsTwoSided] :
    Module.annihilator R (R ⧸ I) = I

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ Module.annihilator R (R ⧸ I) = I

Tactic:
rw [Submodule.annihilator_quotient, colon_top]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_update_eq_ite [DecidableEq α] [DecidableEq M] (f : α → M) (x : α) (y : M) :
    mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Proof state:
α : Type u_1
M : Type u_5
inst✝² : One M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
f : α → M
x : α
y : M
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
rcases eq_or_ne y 1 with rfl | hy <;> simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma sInf_sup_eq : sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

Proof state:
α : Type u
minAx : MinimalAxioms α
s : Set α
b : α
⊢ sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

Tactic:
simpa only [sup_comm] using @sup_sInf_eq α _ s b

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem hasSum_iteratedFDeriv [CharZero 𝕜] {y : E} (hy : y ∈ EMetric.ball 0 r) :
    HasSum (fun n ↦ (n ! : 𝕜)⁻¹ • iteratedFDeriv 𝕜 n f x fun _ ↦ y) (f (x + y))

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) (f (x + y))

Tactic:
convert h.hasSum hy with n

Result:
case h.e'_5.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ EMetric.ball 0 r
n : ℕ
⊢ ((↑n !)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) = (p n) fun x => y

Proof state:
case h.e'_5.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ EMetric.ball 0 r
n : ℕ
⊢ ((↑n !)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) = (p n) fun x => y

Tactic:
rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
  mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/CompTypeclasses.lean
lemma comp_apply
    {φ : M →* N} {ψ : N →* P} {χ : M →* P} (h : CompTriple φ ψ χ) (x : M) :
    ψ (φ x) = χ x

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
⊢ ψ (φ x) = χ x

Tactic:
rw [← h.comp_eq, MonoidHom.comp_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
lemma isIso_counit_app_iff_mem_essImage [L.Faithful] [L.Full] {X : D} :
    IsIso (h.counit.app X) ↔ L.essImage X

Proof state:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
w✝ : C
i : L.obj w✝ ≅ X
⊢ IsIso (h.counit.app (L.obj w✝))

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
w✝ : C
i : L.obj w✝ ≅ X
⊢ IsIso (h.counit.app X)

Tactic:
rw [NatTrans.isIso_app_iff_of_iso _ i.symm]

Result:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
w✝ : C
i : L.obj w✝ ≅ X
⊢ IsIso (h.counit.app (L.obj w✝))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) ↔ L.essImage X

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) → L.essImage X

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ L.essImage X → IsIso (h.counit.app X)

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) → L.essImage X

Tactic:
intro

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
a✝ : IsIso (h.counit.app X)
⊢ L.essImage X

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ L.essImage X → IsIso (h.counit.app X)

Tactic:
rintro ⟨_, ⟨i⟩⟩

Result:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
w✝ : C
i : L.obj w✝ ≅ X
⊢ IsIso (h.counit.app X)

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
a✝ : IsIso (h.counit.app X)
⊢ L.essImage X

Tactic:
exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem toTwoUniqueProds_of_group {G}
    [Group G] [UniqueProds G] : TwoUniqueProds G where
  uniqueMul_of_one_lt_card {A B} hc

Proof state:
case neg.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
x✝ : Mul (Finset G) := Finset.mul
D : Finset G
hD : 1 ∈ D
C : Finset G
hC : 1 ∈ C
hcard : 1 < #C ∨ 1 < #D
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
rcases hcard with hC | hD

Result:
case neg.intro.inl
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
x✝ : Mul (Finset G) := Finset.mul
D : Finset G
hD : 1 ∈ D
C : Finset G
hC✝ hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hC : 1 < #C
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

case neg.intro.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
x✝ : Mul (Finset G) := Finset.mul
D : Finset G
hD✝ : 1 ∈ D
C : Finset G
hC hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hD : 1 < #D
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
/-- See `Finset.Nonempty.card_pow_mono` for a version that works for zero powers. -/
@[to_additive "See `Finset.Nonempty.card_nsmul_mono` for a version that works for zero scalars."]
lemma card_pow_mono (hm : m ≠ 0) (hmn : m ≤ n) : (s ^ m).card ≤ (s ^ n).card

Proof state:
case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(∅ ^ m) ≤ #(∅ ^ n)

Tactic:
simp [hm]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(∅ ^ m) ≤ #(∅ ^ n)

case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)

Proof state:
case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
exact hs.card_pow_mono hmn

Result:
no goals