mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim 0 (f + g) (inl i) = (Sum.elim 0 f + Sum.elim 0 g) (inl i)

pp: case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim 0 (f + g) (inr i) = (Sum.elim 0 f + Sum.elim 0 g) (inr i)

Tactic:
<;>

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim 0 (f + g) (inl i) = (Sum.elim 0 f + Sum.elim 0 g) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim 0 (f + g) (inr i) = (Sum.elim 0 f + Sum.elim 0 g) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : κ
⊢ Sum.elim 0 (t • f) (inl i) = ((RingHom.id R) t • Sum.elim 0 f) (inl i)

pp: case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : ι
⊢ Sum.elim 0 (t • f) (inr i) = ((RingHom.id R) t • Sum.elim 0 f) (inr i)

Tactic:
<;>

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : κ
⊢ Sum.elim 0 (t • f) (inl i) = ((RingHom.id R) t • Sum.elim 0 f) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : ι
⊢ Sum.elim 0 (t • f) (inr i) = ((RingHom.id R) t • Sum.elim 0 f) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim (f + g) 0 (inl i) = (Sum.elim f 0 + Sum.elim g 0) (inl i)

pp: case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim (f + g) 0 (inr i) = (Sum.elim f 0 + Sum.elim g 0) (inr i)

Tactic:
<;>

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim (f + g) 0 (inl i) = (Sum.elim f 0 + Sum.elim g 0) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim (f + g) 0 (inr i) = (Sum.elim f 0 + Sum.elim g 0) (inr i)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : ι
⊢ Sum.elim (t • f) 0 (inl i) = ((RingHom.id R) t • Sum.elim f 0) (inl i)

pp: case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : κ
⊢ Sum.elim (t • f) 0 (inr i) = ((RingHom.id R) t • Sum.elim f 0) (inr i)

Tactic:
<;>

Goal state after:
case inl
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : ι
⊢ Sum.elim (t • f) 0 (inl i) = ((RingHom.id R) t • Sum.elim f 0) (inl i)

case inr
R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
i : κ
⊢ Sum.elim (t • f) 0 (inr i) = ((RingHom.id R) t • Sum.elim f 0) (inr i)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)

Tactic:
by simp_rw [map_iSup]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →ₗ[R] M₂
p : Submodule R M
⊢ ∀ (x y : M →ₗ[R] M₂), (x + y).domRestrict p = x.domRestrict p + y.domRestrict p

Tactic:
simp [LinearMap.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →ₗ[R] M₂
p : Submodule R M
⊢ ∀ (m : R) (x : M →ₗ[R] M₂), (m • x).domRestrict p = (RingHom.id R) m • x.domRestrict p

Tactic:
simp [LinearMap.ext_iff]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : FunLike F α β
f : α → β
s : Set (Set β)
⊢ ⋃ t ∈ s, f ⁻¹' t = sSup (preimage f '' s)

Tactic:
by simp only [Set.sSup_eq_sUnion, Set.sUnion_image]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
this : ∃ x, x ∈ p
⊢ ∀ (x : M₂), x ∈ map 0 p ↔ x ∈ ⊥

Tactic:
simp [this, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: case H
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f q ≤ comap f p ↔ q ≤ p

pp: case H'
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f p ≤ comap f q ↔ p ≤ q

Tactic:
<;>

Goal state after:
case H
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f q ≤ comap f p ↔ q ≤ p

case H'
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f p ≤ comap f q ↔ p ≤ q
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: case pos
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a = 0
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

pp: case neg
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : ¬a = 0
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
<;>

Goal state after:
case pos
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a = 0
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

case neg
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : ¬a = 0
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: case pos
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a = 0
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

pp: case neg
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : ¬a = 0
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
<;>

Goal state after:
case pos
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a = 0
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

case neg
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : ¬a = 0
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: case zero
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
⊢ ↑0 ∈ s

pp: case succ
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n✝ : ℕ
a✝ : ↑n✝ ∈ s
⊢ ↑(n✝ + 1) ∈ s

Tactic:
<;>

Goal state after:
case zero
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
⊢ ↑0 ∈ s

case succ
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n✝ : ℕ
a✝ : ↑n✝ ∈ s
⊢ ↑(n✝ + 1) ∈ s
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ∈ s

Tactic:
← Nat.cast_ofNat

Goal state after:
S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝).1 = (↑x✝).1

pp: case snd
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝).2 = (↑x✝).2

Tactic:
<;>

Goal state after:
case fst
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝).1 = (↑x✝).1

case snd
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝).2 = (↑x✝).2
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)).1 = (-↑(x✝ + 1)).1

pp: case snd
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)).2 = (-↑(x✝ + 1)).2

Tactic:
<;>

Goal state after:
case fst
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)).1 = (-↑(x✝ + 1)).1

case snd
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)).2 = (-↑(x✝ + 1)).2
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).1 = ↑0

pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).1 = ↑n✝
⊢ (↑(n✝ + 1)).1 = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).1 = ↑0

case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).1 = ↑n✝
⊢ (↑(n✝ + 1)).1 = ↑(n✝ + 1)
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).2 = ↑0

pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).2 = ↑n✝
⊢ (↑(n✝ + 1)).2 = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).2 = ↑0

case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).2 = ↑n✝
⊢ (↑(n✝ + 1)).2 = ↑(n✝ + 1)
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case fst
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² * (x✝¹ + x✝)).1 = (x✝² * x✝¹ + x✝² * x✝).1

pp: case snd
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² * (x✝¹ + x✝)).2 = (x✝² * x✝¹ + x✝² * x✝).2

Tactic:
<;>

Goal state after:
case fst
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² * (x✝¹ + x✝)).1 = (x✝² * x✝¹ + x✝² * x✝).1

case snd
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² * (x✝¹ + x✝)).2 = (x✝² * x✝¹ + x✝² * x✝).2
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case fst
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ ((x✝² + x✝¹) * x✝).1 = (x✝² * x✝ + x✝¹ * x✝).1

pp: case snd
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ ((x✝² + x✝¹) * x✝).2 = (x✝² * x✝ + x✝¹ * x✝).2

Tactic:
<;>

Goal state after:
case fst
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ ((x✝² + x✝¹) * x✝).1 = (x✝² * x✝ + x✝¹ * x✝).1

case snd
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ ((x✝² + x✝¹) * x✝).2 = (x✝² * x✝ + x✝¹ * x✝).2
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

pp: case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.nonUnitalSubsemiringClosure

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.nonUnitalSubsemiringClosure
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

pp: case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2.mem
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝¹ x✝ : R
h✝ : x✝ ∈ ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

pp: case refine_2.zero
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ 0 ∈ NonUnitalSubsemiring.closure ↑M

pp: case refine_2.add
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure ↑M
hy✝ : y✝ ∈ AddSubmonoid.closure ↑M
a✝¹ : x✝ ∈ NonUnitalSubsemiring.closure ↑M
a✝ : y✝ ∈ NonUnitalSubsemiring.closure ↑M
⊢ x✝ + y✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
<;>

Goal state after:
case refine_2.mem
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝¹ x✝ : R
h✝ : x✝ ∈ ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

case refine_2.zero
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ 0 ∈ NonUnitalSubsemiring.closure ↑M

case refine_2.add
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure ↑M
hy✝ : y✝ ∈ AddSubmonoid.closure ↑M
a✝¹ : x✝ ∈ NonUnitalSubsemiring.closure ↑M
a✝ : y✝ ∈ NonUnitalSubsemiring.closure ↑M
⊢ x✝ + y✝ ∈ NonUnitalSubsemiring.closure ↑M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
⊢ x✝ ∈ Subsemiring.closure ↑M

pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.subsemiringClosure

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
⊢ x✝ ∈ Subsemiring.closure ↑M

case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.subsemiringClosure
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a b : M
inst✝ : Subsingleton Mˣ
hab : Irreducible (a * b)
⊢ a = 1 ∨ b = 1

Tactic:
by simpa using hab.isUnit_or_isUnit rfl

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a → p ∣ a

pp: case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f b → p ∣ b

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a → p ∣ a

case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f b → p ∣ b
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case e'_3
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ g (f p) = p

pp: case e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ g (f a) = a

Tactic:
<;>

Goal state after:
case e'_3
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ g (f p) = p

case e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ g (f a) = a
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case e'_3
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ g (f p) = p

pp: case e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ g (f b) = b

Tactic:
<;>

Goal state after:
case e'_3
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ g (f p) = p

case e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ g (f b) = b