mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Injective

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ (ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l)) x = (ModuleCat.Hom.hom g) x

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ (n * n).negOnePow = n.negOnePow

Tactic:
simpa using

Goal state after:
n : ℤ
⊢ Even (n * n - n)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g :: l).prod c

Tactic:
simpa using

Goal state after:
case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g * l.prod) c
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
x : α
⊢ f (a • x + c) = f (a • x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x ↦ f (a⁻¹ • x)) (a • c)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
x : α
⊢ f (x - c) = f x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
x : α
⊢ f (x - c) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : SubtractionCommMonoid α
h : Periodic f c
⊢ f (c - x) = f (-x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : SubtractionCommMonoid α
h : Periodic f c
⊢ f (-x + c) = f (-x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
⊢ Periodic f (-c)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
⊢ ∀ (x : α), f (x + -c) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddSemigroup α
h : Periodic f c
a x : α
⊢ (fun x ↦ f (a + x)) (x + c) = (fun x ↦ f (a + x)) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddSemigroup α
h : Periodic f c
a x : α
⊢ f (a + (x + c)) = f (a + x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ (fun x ↦ f (x + a)) (x + c) = (fun x ↦ f (x + a)) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ f (x + c + a) = f (x + a)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : SubtractionCommMonoid α
h : Periodic f c
a : α
⊢ Periodic (fun x ↦ f (x - a)) c

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : SubtractionCommMonoid α
h : Periodic f c
a : α
⊢ Periodic (fun x ↦ f (x + -a)) c
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : NonAssocSemiring α
h : Periodic f c
n : ℕ
⊢ Periodic f (↑n * c)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : NonAssocSemiring α
h : Periodic f c
n : ℕ
⊢ Periodic f (↑n * c)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ f (x - n • c) = f x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ f (x + -(n • c)) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (x - ↑n * c) = f x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (x - ↑n * c) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (↑n * c - x) = f (-x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (-x + ↑n * c) = f (-x)
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
Q : Type v
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : Q ≃ₗ[R] M
h : Baer R Q
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] Q
h' : ∀ (x : R) (mem : x ∈ I), g' x = (↑e.symm ∘ₗ g) ⟨x, mem⟩
⊢ ∀ (x : R) (mem : x ∈ I), (↑e ∘ₗ g') x = g ⟨x, mem⟩

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁴ : Ring R
Q : Type v
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : Q ≃ₗ[R] M
h : Baer R Q
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] Q
h' : ∀ (x : R) (mem : x ∈ I), g' x = (↑e.symm ∘ₗ g) ⟨x, mem⟩
⊢ ∀ (x : R) (mem : x ∈ I), e (g' x) = g ⟨x, mem⟩
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case ofNat
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

Tactic:
simpa using

Goal state after:
case ofNat
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)

Tactic:
simpa using

Goal state after:
case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (-((n + 1) • c))
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℤ
⊢ Periodic f (↑n * c)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℤ
⊢ Periodic f (↑n * c)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddZeroClass α
h : Periodic f c
⊢ f c = f 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddZeroClass α
h : Periodic f c
⊢ f c = f 0
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddZeroClass α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f c = -f 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddZeroClass α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f c = -f 0
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : SubtractionCommMonoid α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f (c - x) = -f (-x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : SubtractionCommMonoid α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f (-x + c) = -f (-x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Antiperiodic f (-c)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ ∀ (x : α), f (x + -c) = -f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ f (-c) = -f 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ f (-c) = -f 0
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq : ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄, ↑a.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ a = b

Tactic:
rcases a with ⟨a, a_le, e1⟩
  congr
  exact LinearPMap.ext domain_eq to_fun_eq

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x - n • c) = ↑n.negOnePow • f x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x + -(n • c)) = ↑n.negOnePow • f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x + ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x + ↑n * c) = ↑↑n.negOnePow * f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x - ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x - ↑n * c) = ↑↑n.negOnePow * f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (↑n * c - x) = ↑↑n.negOnePow * f (-x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (↑n * c - x) = ↑↑n.negOnePow * f (-x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x ↦ f (a + x)) (x + c) = -(fun x ↦ f (a + x)) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ f (a + (x + c)) = -f (a + x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x ↦ f (x + a)) (x + c) = -(fun x ↦ f (x + a)) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ f (x + c + a) = -f (x + a)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : SubtractionCommMonoid α
inst✝ : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic (fun x ↦ f (x - a)) c

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : SubtractionCommMonoid α
inst✝ : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic (fun x ↦ f (x + -a)) c
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = -(fun x ↦ f (a • x)) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
x : α
⊢ f (a • x + c) = -f (a • x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (fun x ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (fun x ↦ f (a⁻¹ • x)) (a • c)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ - c₂)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ + -c₂)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ + -c₂)
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (b ^ n) (b ^ (n + 1)))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (b ^ n) (b ^ (n + 1)))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (b ^ n) (b ^ (n + 1)))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (b ^ n) (b ^ (n + 1)))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (b ^ n) (b ^ (n + 1)))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (b ^ n) (b ^ (n + 1)))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (a + ↑n) (a + ↑n + 1))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (a + ↑n) (a + ↑n + 1))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (a + ↑n) (a + ↑n + 1))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (a + ↑n) (a + ↑n + 1))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (a + ↑n) (a + ↑n + 1))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (a + ↑n) (a + ↑n + 1))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ico (↑n) (↑n + 1))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ico (↑n) (↑n + 1))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (↑n) (↑n + 1))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioo (↑n) (↑n + 1))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (↑n) (↑n + 1))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (↑n) (↑n + 1))
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False

Tactic:
simpa using

Goal state after:
p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = n ↔ ∀ n' < n, p n'

Tactic:
simpa using

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) = n ↔ ∀ n' < n, p n'
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
⊢ motive (p ^ 0 * a)

Tactic:
simpa using

Goal state after:
case zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
⊢ motive a
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ.zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p : ℕ
hp : Prime p
ha : motive (0 + 1)
⊢ motive (p * (0 + 1))

Tactic:
simpa using

Goal state after:
case succ.zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p : ℕ
hp : Prime p
ha : motive (0 + 1)
⊢ motive p
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv R ↥I
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
x : R
mx : x ∈ I
⊢ (g' ∘ₗ ↑eR.symm) x = g ⟨x, mx⟩

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv R ↥I
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
x : R
mx : x ∈ I
⊢ g' ((equivShrink R) x) = g ⟨x, mx⟩
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ ↥({x ∈ range n | n.Coprime x}) :=
  { toFun := fun m ↦ ⟨↑m, ⋯⟩, invFun := fun m ↦ ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ #({a ∈ range n | n.Coprime a}) = Fintype.card ↥({x ∈ range n | n.Coprime x})

Tactic:
Fintype.card_coe

Goal state after:
n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ ↥({x ∈ range n | n.Coprime x}) :=
  { toFun := fun m ↦ ⟨↑m, ⋯⟩, invFun := fun m ↦ ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ #({a ∈ range n | n.Coprime a}) = #({x ∈ range n | n.Coprime x})
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case inr.inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop

Tactic:
simpa using

Goal state after:
case inr.inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ ⨅ i, ⨅ i_1, 𝓟 (Ici (i_1, i)) = ⨅ i, ⨅ j, 𝓟 (Ici (i, j))
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
hpq : p ≤ q
⊢ (fun p ↦ p.1 ×ˢ p.2) p ⊆ (fun p ↦ p.1 ×ˢ p.2) q

Tactic:
simpa using

Goal state after:
case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
hpq : p ≤ q
⊢ p.1 ×ˢ p.2 ⊆ q.1 ×ˢ q.2
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n

Tactic:
simpa using

Goal state after:
β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∀ k < b, u k < u b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
    Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]

Goal state after:
n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inr.hbd
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simpa using

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∃ a, ∀ (b : ℕ), a ≤ b → p (x b)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
⊢ ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
intro a1 a2 b1 b2 c1 c2 h1 h2

Goal state after:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n

Tactic:
simpa using

Goal state after:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n