mathlib-initiative/mathlib-tactics huggingface dataset:
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
hnonempty : c.Nonempty
⊢ i.range ≤ (LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) ⋯).domain

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Tactic:
by

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
· exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
· exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ btw a b c ∨ btw c b 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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
⊢ f m = ↑(LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) ⋯) ⟨i m, ⋯⟩

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 α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x + n • c) = ↑n.negOnePow • f x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ a ≡ b [PMOD p] ↔ ↑a = ↑b

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 α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x - n • c) = ↑n.negOnePow • 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✝¹ : AddCommGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (n • c - x) = ↑n.negOnePow • 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 α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x + ↑n * c) = ↑↑n.negOnePow * 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 α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x - ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b

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 α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (↑n * c - x) = ↑↑n.negOnePow * f (-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
inst✝ : Fact (Function.Injective ⇑i)
x y : ↥i.range
⊢ f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (x + n • c) = (-1) ^ n • 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✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (x - n • c) = (-1) ^ n • 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✝¹ : AddCommGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (n • c - x) = (-1) ^ n • 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 α
inst✝ : Neg β
h : Antiperiodic 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 α
inst✝ : Neg β
h : Antiperiodic 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.Order.Interval.Set.Group

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic 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 α
inst✝ : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic (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
γ : Type u_3
f : α → β
c : α
inst✝³ : Add α
inst✝² : Monoid γ
inst✝¹ : AddGroup β
inst✝ : DistribMulAction γ β
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (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✝² : 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:
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✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (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 α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic 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₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic 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₁ c₂ : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic 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₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - 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✝¹ : Mul β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f * g) c

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
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)

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✝¹ : DivisionMonoid β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic 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 : α → β
c : α
inst✝² : Add α
inst✝¹ : IsRightCancelAdd α
inst✝ : SubtractionCommMonoid β
hf : Antiperiodic f c
s : Finset α
⊢ ∑ k ∈ Finset.map (addRightEmbedding c) s, f k = -∑ k ∈ s, f k

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
inst✝ : Fact (Function.Injective ⇑i)
m : M
⊢ f m =
    ↑{ domain := i.range, toFun := { toFun := fun x ↦ f (Exists.choose ⋯), map_add' := ⋯, map_smul' := ⋯ } } ⟨i m, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b

Tactic:
by

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

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

Tactic:
by

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

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

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

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

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

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

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

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

Goal state after:
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:
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
inst✝ : Fact (Function.Injective ⇑i)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 ↦ x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ ↑x = ↑⟨a, a_mem⟩ + z • y

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
inst✝ : Fact (Function.Injective ⇑i)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

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
inst✝ : Fact (Function.Injective ⇑i)
y : N
z1 z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 + z2) • y, ⋯⟩ =
    ↑(extensionOfMax i f).toLinearPMap ⟨↑z1 • y, ⋯⟩ + ↑(extensionOfMax i f).toLinearPMap ⟨↑z2 • y, ⋯⟩

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
inst✝ : Fact (Function.Injective ⇑i)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 • z2) • y, ⋯⟩ =
    (RingHom.id R) z1 • ↑(extensionOfMax i f).toLinearPMap ⟨↑z2 • y, ⋯⟩

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ r ∈ ideal i f y

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ (extendIdealTo i f h y) r = 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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) r = (extendIdealTo i f h y) r'

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
hr : r • y ∈ (extensionOfMax i f).domain
⊢ (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
⊢ ↑(fst i x) - a = (r - snd i x) • y

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ (r - snd i x) • ?m.277 ∈ (extensionOfMax i f).domain

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
m n : ℕ
hnm : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hnm : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑d ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
a : ↥(extensionOfMax i f).domain
r : R
eq1 : ↑x = ↑a + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap a + (extendIdealTo i f h y) r

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addRightEmbedding a) s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 0 = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = #({x ∈ range n | p x})

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ n

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + if p n then 1 else 0

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ (n : ℕ), count p n ≤ count p (n + 1)

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count p a + count (fun k ↦ p (a + k)) b

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun k ↦ p (k + b)) a + count p b

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 1 = if p 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n < count p (n + 1) ↔ p n

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + 1 ↔ p n

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n ↔ ¬p n

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ n < m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a b m n✝ p : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
⊢ motive (k + 2)

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
by

Goal state after: