mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (if ha : a = 0 then 0 else Classical.choose ⋯) = Classical.choose ⋯

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (if ha : a = 0 then 0 else Classical.choose ⋯) = Classical.choose ⋯
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ (p.mapQ q f h ∘ₛₗ p.mkQ) x = (q.mkQ ∘ₛₗ f) x

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ (p.mapQ q f h ∘ₛₗ p.mkQ) x = (q.mkQ ∘ₛₗ f) x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)

Tactic:
simp only [Module.End.iterate_succ]
    rw [mapQ_comp, ih]
    exact p.le_comap_pow_of_le_comap h k

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ a ≤ x → a = x → x ≤ b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ a ≤ x → a = x → x ≤ b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x = succ b ∨ x ≤ b → x = succ b → a ≤ x

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x = succ b ∨ x ≤ b → x = succ b → a ≤ x
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
x✝ : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel) x ∈ map p.mkQ (comap f q)

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
x✝ : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel) x ∈ map p.mkQ (comap f q)
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
x : α
⊢ x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ b)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
x : α
⊢ x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ b)
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ comap f q ≤ comap (p.liftQ f h ∘ₛₗ p.mkQ) q

Tactic:
liftQ_mkQ

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ comap f q ≤ comap f q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M
⊢ (f.coprod g ∘ₗ inl R M M₂) x✝ = f x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M
⊢ (f.coprod g ∘ₗ inl R M M₂) x✝ = f x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M₂
⊢ (f.coprod g ∘ₗ inr R M M₂) x✝ = g x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M₂
⊢ (f.coprod g ∘ₗ inr R M M₂) x✝ = g x✝
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel) x ∈ ↑q
⊢ (p.liftQ f h) (Quot.mk (⇑p.quotientRel) x) ∈ map f (comap p.mkQ q)

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel) x ∈ ↑q
⊢ (p.liftQ f h) (Quot.mk (⇑p.quotientRel) x) ∈ map f (comap p.mkQ q)
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ (inl R M M₂).coprod (inr R M M₂) = id

Tactic:
by
  ext <;>
    simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (fst R M M₂) x✝ = (id.coprod 0) x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (fst R M M₂) x✝ = (id.coprod 0) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (snd R M M₂) x✝ = (coprod 0 id) x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (snd R M M₂) x✝ = (coprod 0 id) x✝
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ ↑(comap p.mkQ q)
⊢ f x ∈ map (p.liftQ f h) q

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ ↑(comap p.mkQ q)
⊢ f x ∈ map (p.liftQ f h) q
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ≤ b → x = b → a ≤ x

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ≤ b → x = b → a ≤ x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x = pred a ∨ a ≤ x → x = pred a → x ≤ b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x = pred a ∨ a ≤ x → x = pred a → x ≤ b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
x : α
⊢ x ∈ insert (pred a) (Ico a b) ↔ x ∈ Ico (pred a) b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
x : α
⊢ x ∈ insert (pred a) (Ico a b) ↔ x ∈ Ico (pred a) b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H) (p.mkQ x) = p'.mkQ x

Tactic:
factor_mk

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ p'.mkQ x = p'.mkQ x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
fst✝ : M₃
snd✝ : M₄
⊢ (fst✝, snd✝) ∈ (f.prodMap g).range ↔ (fst✝, snd✝) ∈ f.range.prod g.range

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
fst✝ : M₃
snd✝ : M₄
⊢ (fst✝, snd✝) ∈ (f.prodMap g).range ↔ (fst✝, snd✝) ∈ f.range.prod g.range
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : (i : ι) → AddCommMonoid (ψ i)
inst✝² : (i : ι) → Module R (ψ i)
inst✝¹ : (i : ι) → AddCommMonoid (χ i)
inst✝ : (i : ι) → Module R (χ i)
e : (i : ι) → φ i ≃ₗ[R] ψ i
c : R
f : (i : ι) → φ i
x✝ : ι
⊢ (e x✝) ((c • f) x✝) = ((RingHom.id R) c • fun i ↦ (e i) (f i)) x✝

Tactic:
;

Goal state after:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : (i : ι) → AddCommMonoid (ψ i)
inst✝² : (i : ι) → Module R (ψ i)
inst✝¹ : (i : ι) → AddCommMonoid (χ i)
inst✝ : (i : ι) → Module R (χ i)
e : (i : ι) → φ i ≃ₗ[R] ψ i
c : R
f : (i : ι) → φ i
x✝ : ι
⊢ (e x✝) ((c • f) x✝) = ((RingHom.id R) c • fun i ↦ (e i) (f i)) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ comap (fst R M M₂) p ↔ (x, y) ∈ p.prod ⊤

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ comap (fst R M M₂) p ↔ (x, y) ∈ p.prod ⊤
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ comap (snd R M M₂) q ↔ (x, y) ∈ ⊤.prod q

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ comap (snd R M M₂) q ↔ (x, y) ∈ ⊤.prod q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (inl R M M₂) (p.prod q) ↔ x✝ ∈ p

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (inl R M M₂) (p.prod q) ↔ x✝ ∈ p
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x✝ : M₂
⊢ x✝ ∈ comap (inr R M M₂) (p.prod q) ↔ x✝ ∈ q

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x✝ : M₂
⊢ x✝ ∈ comap (inr R M M₂) (p.prod q) ↔ x✝ ∈ q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M
⊢ x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M
⊢ x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M₂
⊢ x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q

Tactic:
;

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M₂
⊢ x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (m : R) (x : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (m • x) = (RingHom.id R) m • (Equiv.sumArrowEquivProdArrow α β M).toFun x

Tactic:
intro r

Goal state after:
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ∀ (x : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (r • x) = (RingHom.id R) r • (Equiv.sumArrowEquivProdArrow α β M).toFun x
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.mem
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
i : ι
⊢ (fun i ↦ single (Sum.inl i) 1) i (Sum.inr k) = 0

Tactic:
;

Goal state after:
case refine_1.mem
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
i : ι
⊢ (fun i ↦ single (Sum.inl i) 1) i (Sum.inr k) = 0
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ hs.toFinset → r (f a✝) (f x✝)

Tactic:
;

Goal state after:
α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ hs.toFinset → r (f a✝) (f x✝)