mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ ∀ (Y : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements)
    (m : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X)) ⟶ Y),
    m = ⟨shrinkYonedaObjObjEquiv Y.snd, ⋯⟩

Tactic:
by

Goal state after:
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
⊢ f ≫ ModuleCat.ofHom l = g

Tactic:
by

Goal state after:
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 : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    Injective ⇑(ConcreteCategory.hom c.inl) ∧
      Injective ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsColimit (BinaryCofan.mk f (↾Subtype.val))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F✝ : C → Type v
J : Type v
F : J → Type (max v u)
s : Cocone (Discrete.functor F)
m :
  { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun x ↦ ⟨j, x⟩ }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    { pt := (j : J) × F j,
                ι :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun x ↦ ⟨j, x⟩ }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m = ↾fun x ↦ (ConcreteCategory.hom (s.ι.app { as := x.fst })) x.snd

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
I : Ideal ℤ
g : ↥I →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul ((z₁ * z₂) • au) = Additive.toMul (z₁ • z₂ • au)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul ((z₁ + z₂) • au) = Additive.toMul (z₁ • au + z₂ • au)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = NPow.toPow

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = ZPow.toPow

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ u ^ ↑n = u ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ u ^ ↑z = u ^ z

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
x✝ : A
⊢ (if x : 0 = 0 then 1 else ⋯.choose) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else ⋯.choose) ^ n✝ = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
⊢ (n✝ • if hn : n✝ = 0 then 0 else Exists.choose ⋯) = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
q : 𝕜
⊢ q / ↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ n • (q / ↑n) = q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
⊢ (match n with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      n =
    a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ RootableBy.root a ↑n ^ n = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (RootableBy.root y n) ^ n = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ Order.succ^[(b - a).toNat] a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ Order.pred^[(b - a).toNat] b = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ (n + 1).negOnePow = -n.negOnePow

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : Even n
⊢ n.negOnePow = 1

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : Odd n
⊢ n.negOnePow = -1

Tactic:
by

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

Goal state before:
pp: case mp
n : ℤ
⊢ n.negOnePow = 1 → Even n

Tactic:
intro h
    rw [← Int.not_odd_iff_even]
    intro h'
    simp only [negOnePow_odd _ h'] at h
    contradiction

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

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = 1 ↔ Even n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = -1 ↔ Odd n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ |↑n.negOnePow| = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ |n|.negOnePow = n.negOnePow

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ |n|.negOnePow = n.negOnePow

Tactic:
by
  obtain h | h := abs_choice n <;> simp only [h, negOnePow_neg]

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

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

Tactic:
by

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

Goal state before:
pp: n₁ n₂ : ℤ
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑↑(↑n).negOnePow = (-1) ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℤ
⊢ ↑↑n.negOnePow = (-1) ^ n.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ sbtw a b c ↔ ¬btw c b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIcc a b)ᶜ = cIoo b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝ : Add α
h : Periodic f c
g : β → γ
⊢ Periodic (g ∘ f) c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝¹ : Add α
inst✝ : Add γ
h : Periodic f c
g : γ →ₙ+ α
g_inv : α → γ
hg : RightInverse g_inv ⇑g
x : γ
⊢ (f ∘ ⇑g) (x + g_inv c) = (f ∘ ⇑g) x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝¹ : Add α
inst✝ : Mul β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f * g) c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝¹ : Add α
inst✝ : Div β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f / g) c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : CommMonoid β
ι : Type u_4
f : ι → α → β
s : Finset ι
hs : ∀ i ∈ s, Periodic (f i) c
⊢ ∀ f_1 ∈ List.map f s.toList, Periodic f_1 c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝¹ : Add α
inst✝ : SMul γ β
h : Periodic f c
a : γ
⊢ Periodic (a • f) c

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddSemigroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
⊢ Periodic f (c₁ + c₂)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c d : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b →
    b < d ∧ d < c ∨ d < c ∧ c < b ∨ c < b ∧ b < d → a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass α
f : α → β
x : α
⊢ f (x + 0) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
a : α
⊢ Periodic (fun x ↦ f^[x] a) n ↔ IsPeriodicPt f n a

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
a : ↥(AddSubgroup.zmultiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
a : ↥(AddSubmonoid.multiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples c)) a b
⊢ f a = f b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddMonoid α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Periodic f (2 • c)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddMonoid α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
by

Goal state after:
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
n : ℤ
⊢ Periodic f ((2 * n) • c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
⊢ Baer R M ↔ ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))

Tactic:
by

Goal state after:
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
n : ℤ
⊢ Antiperiodic f ((2 * n + 1) • c)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
x : α
⊢ f (x - c) = -f x

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
⊢ f (↑0 * c) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(n + 1) * c) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑↑n * c) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ btw a b c → btw c b a → a = b ∨ b = c ∨ c = a

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
x✝² x✝¹ : ExtensionOf i f
x✝ : x✝².toLinearPMap = x✝¹.toLinearPMap
⊢ x✝² = x✝¹

Tactic:
by

Goal state after:
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
X1 X2 : ExtensionOf i f
x : N
hx : x ∈ i.range
⊢ x ∈ X1.eqLocus X2.toLinearPMap

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ioo 0 b ↔ a ∈ Ioo 0 b

Tactic:
by

Goal state after:
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
X Y : ExtensionOf i f
x : N
y : x ∈ (X ⊓ Y).domain
h : x ∈ (X.toLinearPMap ⊓ Y.toLinearPMap).domain
⊢ ↑(X ⊓ Y).toLinearPMap ⟨x, y⟩ = ↑(X.toLinearPMap ⊓ Y.toLinearPMap) ⟨x, h⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(Int.negSucc n) * c) = 0

Tactic:
by

Goal state after:
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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) ((fun x ↦ x.toLinearPMap) '' c)

Tactic:
by

Goal state after: