Theorem: DividedPowers.OfInvertibleFactorial.foo (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Tactic:
rw [Finset.mem_antidiagonal] at hk
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! = ↑m ! * Ring.inverse ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! = ↑m ! * Ring.inverse ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! * ↑k.1! = ↑m !

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! * ↑k.1! = ↑m !
Tactic:
rw [← hk, ← Nat.cast_mul, ← Nat.cast_mul, add_comm, Nat.add_choose_mul_factorial_mul_factorial]
State after:
no goals

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.1!
Tactic:
apply factorial_isUnit' hm
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ m

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ m
Tactic:
rw [← hk]
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ k.1 + k.2

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.1 ≤ k.1 + k.2
Tactic:
exact Nat.le_add_right k.1 k.2
State after:
no goals

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!
Tactic:
apply factorial_isUnit' hm
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ m

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ m
Tactic:
rw [← hk]
State after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ k.1 + k.2

State before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ k.2 ≤ k.1 + k.2
Tactic:
exact Nat.le_add_left k.2 k.1
State after:
no goals