Theorem: exists_irrationals_pow_rational (GroupComp/PowerIrrationals.lean)

State before:
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
let b := Real.sqrt 2
State after:
b : ℝ := Real.sqrt 2
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

State before:
b : ℝ := Real.sqrt 2
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
by_cases c:Irrational (b ^ b)
State after:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

case neg
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

State before:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
let a := b ^ b
State after:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

State before:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
use a, b
State after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

State before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
simp [irrational_sqrt_two, c, sq2_pow_twice]
State after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ¬Irrational 2

State before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ¬Irrational 2
Tactic:
simp [irrational_iff_ne_rational]
State after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ x x_1, 2 = ↑x / ↑x_1

State before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ x x_1, 2 = ↑x / ↑x_1
Tactic:
use 2, 1
State after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ 2 = ↑2 / ↑1

State before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ 2 = ↑2 / ↑1
Tactic:
simp
State after:
no goals

State before:
case neg
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
use b, b
State after:
case h
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ Irrational b ∧ Irrational b ∧ ¬Irrational (b ^ b)

State before:
case h
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ Irrational b ∧ Irrational b ∧ ¬Irrational (b ^ b)
Tactic:
simp [irrational_sqrt_two, c]
State after:
no goals