Theorem: IMOSL.IMO2010A1.indicator_const_is_good (IMOSLLean4/IMO2010/A1/A1Monoid.lean)

State before:
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
⊢ (fun n => if n ∈ A then C else 0) (m * n) =
    (fun n => if n ∈ A then C else 0) m * ↑⌊(fun n => if n ∈ A then C else 0) n⌋
Tactic:
simp only [h]
State after:
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋

State before:
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Tactic:
by_cases h1 : n ∈ A
State after:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋

case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋

State before:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Tactic:
rw [if_pos h1, h0, Int.cast_one, mul_one]
State after:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = if m ∈ A then C else 0

State before:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = if m ∈ A then C else 0
Tactic:
exact if_congr (and_iff_left h1) rfl rfl
State after:
no goals

State before:
case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Tactic:
rw [if_neg h1, Int.floor_zero, Int.cast_zero, mul_zero]
State after:
case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = 0

State before:
case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = 0
Tactic:
exact if_neg λ h2 ↦ h1 h2.2
State after:
no goals