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

Tactic:
]

Goal state after:
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.fst i a) + ExtensionOfMaxAdjoin.snd i a • y +
      (↑(ExtensionOfMaxAdjoin.fst i b) + ExtensionOfMaxAdjoin.snd i b • y) =
    ↑(ExtensionOfMaxAdjoin.fst i a) + ↑(ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a • y + ExtensionOfMaxAdjoin.snd i b • y)
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
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 = k + 2

Tactic:
]

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

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

Tactic:
]

Goal state after:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)
Module: Mathlib.Algebra.Group.Nat.Range

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

Tactic:
]

Goal state after:
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case convert_1
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
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ^ t.succ ∣ k + 2

Tactic:
]

Goal state after:
case convert_1
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
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ^ t.succ ∣ k + 2
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (List.filter (fun b ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})

Tactic:
]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (List.filter (fun b ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})
Module: Mathlib.Data.Nat.Count

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

pp: case s
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Finset ℕ

pp: case H
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ ?s ↔ x < n ∧ p x

Tactic:
]

Goal state after:
case H
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x
Module: Mathlib.Data.Nat.Count

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

Tactic:
]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ n
Module: Mathlib.Data.Nat.Count

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

Tactic:
]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k ↦ p (b + k)) a + count p b = count (fun k ↦ p (k + b)) a + count p b
Module: Mathlib.Data.Nat.Count

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

Tactic:
]

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)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
]

Goal state after:
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)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ #hp.toFinset

Tactic:
]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ #hp.toFinset
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
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y

Tactic:
]

Goal state after:
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
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x

Tactic:
]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n)

Tactic:
]

Goal state after:
case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n)
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
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r •
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a)) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
]

Goal state after:
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
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r •
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a)) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun x ↦ p x) ∘ fun x ↦ x % a) (Ico n (n + a)))

Tactic:
]

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun x ↦ p x) ∘ fun x ↦ x % a) (Ico n (n + a)))
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ
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
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p * (p ^ n * a))

Tactic:
]

Goal state after:
case succ
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
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p * (p ^ n * a))
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
m : M
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨i m, ⋯⟩ = ↑(extensionOfMax i f).toLinearPMap ⟨i m, ?m.544⟩

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
m : M
⊢ i m ∈ (extensionOfMax i f).domain

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
m : M
⊢ ↑⟨i m, ⋯⟩ = ↑⟨i m, ?m.544⟩ + 0 • y

Tactic:
]

Goal state after:
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
m : M
⊢ ↑⟨i m, ⋯⟩ = ↑⟨i m, ⋯⟩ + 0 • y
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 : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMax i f).toLinearPMap x = ↑(extensionOfMax i f).toLinearPMap x

Tactic:
]

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
⊢ ∃ y_1 ∈ (extensionOfMax i f).domain, ∃ z ∈ R ∙ ?y, y_1 + z = y

pp: case y
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
⊢ N

Tactic:
]

Goal state after:
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
⊢ ∃ y_1 ∈ (extensionOfMax i f).domain, ∃ z ∈ R ∙ ?y, y_1 + z = y

case y
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
⊢ N
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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)

Tactic:
]

Goal state after:
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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)
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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨x, ⋯⟩)

Tactic:
]

Goal state after:
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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨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
h : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f

Goal state after:
R : Type u
inst✝² : Ring R
Q : Type v
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
h✝ : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
h : Y →ₗ[R] Q
H : h ∘ₗ i = f
⊢ ∃ h, ∀ (x : X), h (i x) = f x
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k ↦ f (p ^ k)

Tactic:
]

Goal state after:
case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ ((a.factorization + b.factorization).prod fun p k ↦ f (p ^ k)) =
    (a.factorization + b.factorization).prod fun p k ↦ f (p ^ k)

pp: case coprime.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support

Tactic:
]

Goal state after:
case coprime.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support
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}) = #({x ∈ range n | n.Coprime x})

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: a n : ℕ
⊢ #({x ∈ range a | a.Coprime x}) = #({a_1 ∈ range a | a.Coprime a_1})

pp: case pp
a n : ℕ
⊢ Function.Periodic (fun x ↦ a.Coprime x) a

Tactic:
]

Goal state after:
case pp
a n : ℕ
⊢ Function.Periodic (fun x ↦ a.Coprime x) a
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * (0 + 1)

Tactic:
]

Goal state after:
case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * (0 + 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x} ∪
        {x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) +
      #({x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})

Tactic:
]

Goal state after:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x} ∪
        {x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) +
      #({x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ φ a * (i + 1) + φ a ≤ φ a * (i + 1) + φ a

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ

Tactic:
]

Goal state after:
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = 2

Tactic:
]

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ

Tactic:
]

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

Goal state before:
pp: case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})

Tactic:
]

Goal state after:
case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.hi
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ d = d

Tactic:
]

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

Goal state before:
pp: d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ (d * x).gcd b ∣ b

Tactic:
]

Goal state after:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ (d * x).gcd b ∣ b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : x.gcd q = 1
⊢ x.Coprime q

Tactic:
]

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : x.gcd q = 1
⊢ x.Coprime q
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Tactic:
]

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
]

Goal state after:
n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ ∑ d ∈ n.divisors, φ (n / d) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
]

Goal state after:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ ∑ d ∈ n.divisors, φ (n / d) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (0 + 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

pp: case e'_2.hab
n : ℕ
⊢ 0 < n.succ

Tactic:
]

Goal state after:
case e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (0 + 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

case e'_2.hab
n : ℕ
⊢ 0 < n.succ