Theorem: Nat.bitwise_comm (Algdata/Data/Nat/Bits.lean)

State before:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m
Tactic:
have : flip f = f := funext (λ a => funext (λ b => h b a))
State after:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m

State before:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m
Tactic:
intro m n
State after:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
m n : Nat
⊢ bitwise f m n = bitwise f n m

State before:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
m n : Nat
⊢ bitwise f m n = bitwise f n m
Tactic:
rw [←bitwise_flip (m:=m) (n:=n), this]
State after:
no goals