Theorem: n1_2_24 (AlgebraI/Subgroups.lean)

State before:
⊢ ∃ G x, (∀ (g : G), IsOfFinAddOrder g) ∧ AddMonoid.exponent G = 0
Tactic:
refine' ⟨ℚ ⧸ AddSubgroup.zmultiples (1 : ℚ), inferInstance, fun g => _, _⟩
State after:
case refine'_1
g : ℚ ⧸ AddSubgroup.zmultiples 1
⊢ IsOfFinAddOrder g

case refine'_2

⊢ AddMonoid.exponent (ℚ ⧸ AddSubgroup.zmultiples 1) = 0

State before:
case refine'_1
g : ℚ ⧸ AddSubgroup.zmultiples 1
⊢ IsOfFinAddOrder g
Tactic:
induction g using QuotientAddGroup.induction_on' with | H g => ?_
State after:
case refine'_1.H
g : ℚ
⊢ IsOfFinAddOrder ↑g

State before:
case refine'_1.H
g : ℚ
⊢ IsOfFinAddOrder ↑g
Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]
State after:
case refine'_1.H
g : ℚ
⊢ ∃ n, 0 < n ∧ n • ↑g = 0

State before:
case refine'_1.H
g : ℚ
⊢ ∃ n, 0 < n ∧ n • ↑g = 0
Tactic:
refine' ⟨g.den, g.pos, _⟩
State after:
case refine'_1.H
g : ℚ
⊢ g.den • ↑g = 0

State before:
case refine'_1.H
g : ℚ
⊢ g.den • ↑g = 0
Tactic:
rw [← QuotientAddGroup.mk_nsmul, nsmul_eq_mul, QuotientAddGroup.eq_zero_iff,
  AddSubgroup.mem_zmultiples_iff]
State after:
case refine'_1.H
g : ℚ
⊢ ∃ k, k • 1 = ↑g.den * g

State before:
case refine'_1.H
g : ℚ
⊢ ∃ k, k • 1 = ↑g.den * g
Tactic:
use g.num
State after:
case h
g : ℚ
⊢ g.num • 1 = ↑g.den * g

State before:
case h
g : ℚ
⊢ g.num • 1 = ↑g.den * g
Tactic:
rw [Int.smul_one_eq_coe, ← Rat.mul_den_eq_num, mul_comm]
State after:
no goals

State before:
case refine'_2

⊢ AddMonoid.exponent (ℚ ⧸ AddSubgroup.zmultiples 1) = 0
Tactic:
rw [AddMonoid.exponent_eq_zero_iff, AddMonoid.ExponentExists]
State after:
case refine'_2

⊢ ¬∃ n, 0 < n ∧ ∀ (g : ℚ ⧸ AddSubgroup.zmultiples 1), n • g = 0

State before:
case refine'_2

⊢ ¬∃ n, 0 < n ∧ ∀ (g : ℚ ⧸ AddSubgroup.zmultiples 1), n • g = 0
Tactic:
push_neg
State after:
case refine'_2

⊢ ∀ (n : ℕ), 0 < n → ∃ g, n • g ≠ 0

State before:
case refine'_2

⊢ ∀ (n : ℕ), 0 < n → ∃ g, n • g ≠ 0
Tactic:
refine' fun n hn => ⟨(1 / (2 * n) : ℚ), _⟩
State after:
case refine'_2
n : ℕ
hn : 0 < n
⊢ n • ↑(1 / (2 * ↑n)) ≠ 0

State before:
case refine'_2
n : ℕ
hn : 0 < n
⊢ n • ↑(1 / (2 * ↑n)) ≠ 0
Tactic:
rw [← QuotientAddGroup.mk_nsmul, nsmul_eq_mul, Ne.def, QuotientAddGroup.eq_zero_iff,
  AddSubgroup.mem_zmultiples_iff, not_exists]
State after:
case refine'_2
n : ℕ
hn : 0 < n
⊢ ∀ (x : ℤ), ¬x • 1 = ↑n * (1 / (2 * ↑n))

State before:
case refine'_2
n : ℕ
hn : 0 < n
⊢ ∀ (x : ℤ), ¬x • 1 = ↑n * (1 / (2 * ↑n))
Tactic:
refine' fun x => ne_of_apply_ne Rat.den _
State after:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ (x • 1).den ≠ (↑n * (1 / (2 * ↑n))).den

State before:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ (x • 1).den ≠ (↑n * (1 / (2 * ↑n))).den
Tactic:
rw [Int.smul_one_eq_coe, Rat.coe_int_den, one_div, mul_inv_rev, ← mul_assoc,
  mul_inv_cancel ((@Nat.cast_ne_zero ℚ _ _ _).mpr hn.ne'), one_mul, ← Int.cast_two,
  Rat.inv_coe_int_den]
State after:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ 1 ≠ if 2 = 0 then 1 else Int.natAbs 2

State before:
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ 1 ≠ if 2 = 0 then 1 else Int.natAbs 2
Tactic:
norm_num
State after:
no goals