mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • ↑m⁻¹ * g • ↑m = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
⊢ mulAction'.toSMul = instSMulOfMul

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: M : Type u_6
inst✝ : CommMonoid M
u₁ u₂ : Mˣ
⊢ u₁ • u₂ = u₁ * u₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N✝ : Type u_4
α : Type u_5
M : Type u_6
N : Type u_7
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MulDistribMulAction M N
m : M
u : Nˣ
⊢ m • ↑u * m • ↑u⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N✝ : Type u_4
α : Type u_5
M : Type u_6
N : Type u_7
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MulDistribMulAction M N
m : M
u : Nˣ
⊢ m • ↑u⁻¹ * m • ↑u = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorRing R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
H : ∀ (x : K), ∃ n, x < ↑n
x y : K
y0 : 0 < y
n : ℕ
h : x / y < ↑n
⊢ x < n • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
⊢ IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G✝ : Type u_1
M : Type u_2
A✝ : Type u_3
B✝ : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (x * y) • f = x • y • f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G✝ : Type u_1
M : Type u_2
A✝ : Type u_3
B✝ : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ 1 • f = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
m : α
hm : IsUnit m
⊢ Function.Bijective fun a ↦ m • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : MulAction M α
y₁ y₂ : α
H : (fun y x ↦ x • y) y₁ = (fun y x ↦ x • y) y₂
⊢ 1 • y₁ = 1 • y₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ (∀ (x : K), ∃ n, x < ↑n) → Archimedean K

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
⊢ f (c • 1) = f 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x✝ : Archimedean K
x : K
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
x y : B
⊢ f (c • (x * y)) = f (c • x * c • y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ
⊢ q ≤ ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x : K
n : ℤ
h : ↑n < x
⊢ ↑↑n < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ c • 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ ∀ (x y : B), c • (x * y) = c • x * c • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
hR : CovariantClass H H (fun x y ↦ y + x) R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
⊢ R (f x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Add G
inst✝¹ : Add H
a : G
b : H
K : Type u_3
inst✝ : Add K
c : K
g : H →+c[b, c] K
f : G →+c[a, b] H
⊢ ∀ (x : G), (⇑g ∘ ⇑f) (x + a) = (⇑g ∘ ⇑f) x + c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Add G
inst✝² : Add H
a : G
b : H
K : Type u_3
inst✝¹ : VAdd K H
inst✝ : VAddAssocClass K H H
c : K
f : G →+c[a, b] H
x : G
⊢ (c +ᵥ ⇑f) (x + a) = (c +ᵥ ⇑f) x + b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
K : Type u_3
inst✝² : Add G
inst✝¹ : AddZeroClass H
a : G
b : H
inst✝ : DistribSMul K H
c : K
f : G →+c[a, b] H
x : G
⊢ (c • ⇑f) (x + a) = (c • ⇑f) x + c • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a : G
⊢ Multiplicative.toAdd 1 +ᵥ AddConstMap.id = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a : G
x✝¹ x✝ : Multiplicative G
⊢ Multiplicative.toAdd (x✝¹ * x✝) +ᵥ AddConstMap.id =
    (Multiplicative.toAdd x✝¹ +ᵥ AddConstMap.id) * (Multiplicative.toAdd x✝ +ᵥ AddConstMap.id)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
b : H
f : G →+c[a, b] H
x✝ : G
⊢ -f (-(x✝ + a)) = -f (-x✝) + b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
b : H
x✝¹ : G →+c[a, b] H
x✝ : G
⊢ ((fun f ↦ { toFun := fun x ↦ -f (-x), map_add_const' := ⋯ })
        ((fun f ↦ { toFun := fun x ↦ -f (-x), map_add_const' := ⋯ }) x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : ↑(Ico 0 1) → G
x : R
⊢ f ⟨Int.fract (x + 1), ⋯⟩ + ⌊x + 1⌋ • a = f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ 1 < (y - x) * ↑n

Tactic:
← div_lt_iff₀' (sub_pos.2 h),

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ 1 / (y - x) < ↑n
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
⊢ (fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
⊢ ∃ z, x < ↑z / ↑n ∧ ↑z / ↑n < y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
⊢ ∃ q, x < ↑q ∧ ↑q < y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 0 < 1 / δ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 0 ≤ y / δ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
⊢ ∃ m, y ≤ (↑m * δ) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
⊢ ¬y ≤ (↑0 * δ) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
⊢ 0 ≤ q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ max x 0 = y - (y - max x 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ 0 ≤ δ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ (↑m * δ) ^ n - (y - max x 0) < (↑m * δ) ^ n - ((↑m * δ) ^ n - q ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
xqn : max x 0 < q ^ n
⊢ 0 ≤ q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x : K
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℤ
m0 : 0 < m
⊢ ↑n.toNat ≤ n.toNat • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K✝ : Type u_4
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ Archimedean K

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ 0 < y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
⊢ Archimedean (WithBot M)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ 1 < y

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
⊢ MulArchimedean (WithZero M)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : map f l₁ <+~ map f l₂
⊢ l₁ <+~ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : l₁ <+~ l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
⊢ ∀ (a : Multiset α), a.Le a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
⊢ ∀ (a b c : Multiset α), a.Le b → b.Le c → a.Le c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
⊢ ∀ (a b : Multiset α), a.Le b → b.Le a → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
⊢ ∀ {s₂ : Multiset α} {e : ↑l₁ = s₂} {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H =
      ↑(List.pmap f l₁ H₁)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
l : List α
⊢ (∀ (a : α), a ∈ l → p a) ↔ ∀ (a : α), a ∈ ⟦l⟧ → p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type v
γ : Type u_2
m : Multiset α
β : α → Type u_3
inst✝ : (a : α) → DecidableEq (β a)
f g : (a : α) → a ∈ m → β a
⊢ (∀ (a : α) (h : a ∈ m), f a h = g a h) ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (∃ a, a ∈ l ∧ p a) ↔ ∃ x, x ∈ ⟦l⟧ ∧ p x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (a : List α), ↑l = ↑a ∧ List.Pairwise r a ↔ l ~ a ∧ List.Pairwise r a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Multiset α
nodup✝¹ : s.Nodup
t : Multiset α
nodup✝ : t.Nodup
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ (b : α), b ∈ s → ¬a = b) ↔ ¬a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ (b : α), b ∈ s → ¬b = a) ↔ ¬a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ ¬x ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s₁ s₂ : Finset α
⊢ ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
p : α → Prop
_hp : (a : α) → Decidable (p a)
⊢ (∃ a x, p a) ↔ ∃ a, a ∈ s ∧ p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), p a → countP p (a ::ₘ Quot.mk (⇑(isSetoid α)) a_1) = countP p (Quot.mk (⇑(isSetoid α)) a_1) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {p} /ₛ {p} = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), ¬p a → countP p (a ::ₘ Quot.mk (⇑(isSetoid α)) a_1) = countP p (Quot.mk (⇑(isSetoid α)) a_1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
s t : Set P
⊢ 1 ∈ s /ₛ t ↔ ¬Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ /ₛ p = p₂ /ₛ p
⊢ p₁ = p₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ p₁ = p₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
b : α
s : Multiset α
⊢ ∀ (a : List α),
    countP p (b ::ₘ Quot.mk (⇑(isSetoid α)) a) = countP p (Quot.mk (⇑(isSetoid α)) a) + if p b then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) / (p₃ /ₛ p₁) = p₁ /ₛ p₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ card (Quot.mk (⇑(isSetoid α)) l) =
    countP p (Quot.mk (⇑(isSetoid α)) l) + countP (fun x ↦ ¬p x) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
p₁ p₂ : P
⊢ v • p₁ /ₛ v • p₂ = p₁ /ₛ p₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a ↦ p ↑a) (attach ⟦l⟧) = countP p ⟦l⟧

Tactic:
by

Goal state after: