Theorem: Nat.lt_iff_gt (MLIR/Util/KDTensor.lean)

State before:
⊢ ∀ (a b : ℕ), a < b ↔ b > a
Tactic:
intros a b
State after:
a b : ℕ
⊢ a < b ↔ b > a

State before:
a b : ℕ
⊢ a < b ↔ b > a
Tactic:
constructor
State after:
case mp
a b : ℕ
⊢ a < b → b > a

case mpr
a b : ℕ
⊢ b > a → a < b

State before:
a b : ℕ
⊢ a < b → b > a
Tactic:
case mp => {
   intros A_LT_B;
   simp [GT.gt]; exact A_LT_B;
}
State after:
no goals

State before:
a b : ℕ
⊢ b > a → a < b
Tactic:
case mpr => {
  intros B_GT_A;
  simp [GT.gt] at B_GT_A;
  exact B_GT_A;
}
State after:
no goals

State before:
a b : ℕ
⊢ a < b → b > a
Tactic:
intros A_LT_B
State after:
a b : ℕ
A_LT_B : a < b
⊢ b > a

State before:
a b : ℕ
A_LT_B : a < b
⊢ b > a
Tactic:
simp [GT.gt]
State after:
a b : ℕ
A_LT_B : a < b
⊢ a < b

State before:
a b : ℕ
A_LT_B : a < b
⊢ a < b
Tactic:
exact A_LT_B
State after:
no goals

State before:
a b : ℕ
⊢ b > a → a < b
Tactic:
intros B_GT_A
State after:
a b : ℕ
B_GT_A : b > a
⊢ a < b

State before:
a b : ℕ
B_GT_A : b > a
⊢ a < b
Tactic:
simp [GT.gt] at B_GT_A
State after:
a b : ℕ
B_GT_A : a < b
⊢ a < b

State before:
a b : ℕ
B_GT_A : a < b
⊢ a < b
Tactic:
exact B_GT_A
State after:
no goals