-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem divOf_add_modOf (x : k[G]) (g : G) :
    of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x

Proof state:
case H.inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d a : G
ha : a ∈ (x /ᵒᶠ g).support
⊢ g + a = g + d ↔ a = d

Tactic:
exact add_right_inj _

Result:
no goals

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g) g' = x g'

Tactic:
rw [Finsupp.add_apply]

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Result:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (of' k G g * (x /ᵒᶠ g)) (g + d) + (x %ᵒᶠ g) (g + d) = x (g + d)

case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'

Proof state:
case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'

Tactic:
rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
  zero_add]

Result:
no goals

Proof state:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (of' k G g * (x /ᵒᶠ g)) (g + d) = x (g + d)

Tactic:
rw [of'_apply, single_mul_apply_aux _ _ _, one_mul, divOf_apply]

Result:
case H.inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ ∀ a ∈ (x /ᵒᶠ g).support, g + a = g + d ↔ a = d

Proof state:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (of' k G g * (x /ᵒᶠ g)) (g + d) + (x %ᵒᶠ g) (g + d) = x (g + d)

Tactic:
rw [modOf_apply_self_add, add_zero]

Result:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (of' k G g * (x /ᵒᶠ g)) (g + d) = x (g + d)

Proof state:
case H.inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ ∀ a ∈ (x /ᵒᶠ g).support, g + a = g + d ↔ a = d

Tactic:
intro a ha

Result:
case H.inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d a : G
ha : a ∈ (x /ᵒᶠ g).support
⊢ g + a = g + d ↔ a = d

Proof state:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (of' k G g * (x /ᵒᶠ g)) (g + d) + (x %ᵒᶠ g) (g + d) = x (g + d)

case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'

Tactic:
swap

Result:
case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'

case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (of' k G g * (x /ᵒᶠ g)) (g + d) + (x %ᵒᶠ g) (g + d) = x (g + d)

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x

Tactic:
ext g'

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g) g' = x g'