-- Mathlib/GroupTheory/Exponent.lean
theorem Monoid.exponent_prod {M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] :
    exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂)

Proof state:
case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent (M₁ × M₂) ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
refine exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_

Result:
case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1

Proof state:
case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
exact dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _

Result:
no goals

Proof state:
case refine_3
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Tactic:
exact MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective

Result:
no goals

Proof state:
case refine_2
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₁ ∣ exponent (M₁ × M₂)

Tactic:
exact MonoidHom.exponent_dvd (f := MonoidHom.fst M₁ M₂) Prod.fst_surjective

Result:
no goals

Proof state:
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent (M₁ × M₂) = GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)

Result:
case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent (M₁ × M₂) ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

case refine_2
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₁ ∣ exponent (M₁ × M₂)

case refine_3
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Proof state:
case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2

Tactic:
rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]

Result:
case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Proof state:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).1 = 1.1

Tactic:
rw [Prod.pow_fst, Prod.fst_one, ← orderOf_dvd_iff_pow_eq_one]

Result:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Proof state:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)

Tactic:
exact dvd_trans (Monoid.order_dvd_exponent (g.1)) <| dvd_lcm_left _ _

Result:
no goals

Proof state:
case refine_1
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1

Tactic:
ext1

Result:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).1 = 1.1

case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2