mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝
Module: Mathlib.RingTheory.NonUnitalSubring.Defs

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
q : NonUnitalSubring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } =
    (fun s ↦ s.carrier) q
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
q : NonUnitalSubring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } =
    (fun s ↦ s.carrier) q
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } = q
Module: Mathlib.RingTheory.NonUnitalSubring.Defs

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.RingTheory.NonUnitalSubring.Defs

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: case mk
R : Type u
inst✝ : NonAssocRing R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
;

Goal state after:
case mk
R : Type u
inst✝ : NonAssocRing R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: case mk
R : Type u
inst✝ : NonAssocRing R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }.toSubring h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
;

Goal state after:
case mk
R : Type u
inst✝ : NonAssocRing R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }.toSubring h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M) (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : R
snd✝ : S
⊢ (fun x ↦ (x, 0)) (fst✝, snd✝).1 = (fst✝, snd✝)

Tactic:
;

Goal state after:
case mk
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : R
snd✝ : S
⊢ (fun x ↦ (x, 0)) (fst✝, snd✝).1 = (fst✝, snd✝)
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : S
snd✝ : R
⊢ (fun x ↦ (0, x)) (fst✝, snd✝).2 = (fst✝, snd✝)

Tactic:
;

Goal state after:
case mk
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : S
snd✝ : R
⊢ (fun x ↦ (0, x)) (fst✝, snd✝).2 = (fst✝, snd✝)
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : R) (x : ι), a ∈ S x → ∀ (b : R) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ NonUnitalSubring.map f ⊤

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ NonUnitalSubring.map f ⊤
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
r✝ : ℕ
⊢ (algebraMap ℕ R) r✝ = (algebraMap ℕ R) r✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
r✝ : ℕ
⊢ (algebraMap ℕ R) r✝ = (algebraMap ℕ R) r✝
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : ℕ
⊢ (⇑(algebraMap R A) ∘ Nat.cast) x✝ = ↑x✝

Tactic:
;

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : ℕ
⊢ (⇑(algebraMap R A) ∘ Nat.cast) x✝ = ↑x✝
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x✝ : ℤ
⊢ (⇑(algebraMap R A) ∘ Int.cast) x✝ = ↑x✝

Tactic:
;

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x✝ : ℤ
⊢ (⇑(algebraMap R A) ∘ Int.cast) x✝ = ↑x✝
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ (↑↑(φ₁.comp ↑φ₂)).toFun ((algebraMap R A) r) = φ₁ (φ₂ ((algebraMap R A) r))

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ (↑↑(φ₁.comp ↑φ₂)).toFun ((algebraMap R A) r) = φ₁ (φ₂ ((algebraMap R A) r))
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n : ℕ
x✝ : A
⊢ (φ ^ Nat.zero) x✝ = (⇑φ)^[Nat.zero] x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n : ℕ
x✝ : A
⊢ (φ ^ Nat.zero) x✝ = (⇑φ)^[Nat.zero] x✝
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n x✝¹ : ℕ
ih : ⇑(φ ^ x✝¹) = (⇑φ)^[x✝¹]
x✝ : A
⊢ (φ ^ x✝¹.succ) x✝ = (⇑φ)^[x✝¹.succ] x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n x✝¹ : ℕ
ih : ⇑(φ ^ x✝¹) = (⇑φ)^[x✝¹]
x✝ : A
⊢ (φ ^ x✝¹.succ) x✝ = (⇑φ)^[x✝¹.succ] x✝
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² x✝¹ : A →ₐ[R] A
x✝ : Aˣ
⊢ ↑((x✝² * x✝¹) • x✝) = ↑(x✝² • x✝¹ • x✝)

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² x✝¹ : A →ₐ[R] A
x✝ : Aˣ
⊢ ↑((x✝² * x✝¹) • x✝) = ↑(x✝² • x✝¹ • x✝)
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : Aˣ
⊢ ↑(1 • x✝) = ↑x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : Aˣ
⊢ ↑(1 • x✝) = ↑x✝
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A →ₐ[R] A
⊢ ↑(x✝ • 1) = ↑1

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A →ₐ[R] A
⊢ ↑(x✝ • 1) = ↑1
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² : A →ₐ[R] A
x✝¹ x✝ : Aˣ
⊢ ↑(x✝² • (x✝¹ * x✝)) = ↑(x✝² • x✝¹ * x✝² • x✝)

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² : A →ₐ[R] A
x✝¹ x✝ : Aˣ
⊢ ↑(x✝² • (x✝¹ * x✝)) = ↑(x✝² • x✝¹ * x✝² • x✝)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M →ₗ[R] N
x : M
r : R
⊢ f.toFun ((algebraMap R S) r • x) = (RingHom.id S) ((algebraMap R S) r) • f.toFun x

Tactic:
;

Goal state after:
R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M →ₗ[R] N
x : M
r : R
⊢ f.toFun ((algebraMap R S) r • x) = (RingHom.id S) ((algebraMap R S) r) • f.toFun x
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M ≃ₗ[R] N
x : M
r : R
⊢ (↑f).toFun ((algebraMap R S) r • x) = (RingHom.id S) ((algebraMap R S) r) • (↑f).toFun x

Tactic:
;

Goal state after:
R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M ≃ₗ[R] N
x : M
r : R
⊢ (↑f).toFun ((algebraMap R S) r • x) = (RingHom.id S) ((algebraMap R S) r) • (↑f).toFun x
Module: Mathlib.Algebra.Ring.Action.Group

Goal state before:
pp: G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x✝ : R
⊢ (let __src := DistribMulAction.toAddEquiv R 1;
      let __src_1 := toRingHom G R 1;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝ =
    1 x✝

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x✝ : R
⊢ (let __src := DistribMulAction.toAddEquiv R 1;
      let __src_1 := toRingHom G R 1;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝ =
    1 x✝
Module: Mathlib.Algebra.Ring.Action.Group

Goal state before:
pp: G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x y : G
x✝ : R
⊢ (let __src := DistribMulAction.toAddEquiv R (x * y);
      let __src_1 := toRingHom G R (x * y);
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝ =
    ((let __src := DistribMulAction.toAddEquiv R x;
        let __src_1 := toRingHom G R x;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }) *
        let __src := DistribMulAction.toAddEquiv R y;
        let __src_1 := toRingHom G R y;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x y : G
x✝ : R
⊢ (let __src := DistribMulAction.toAddEquiv R (x * y);
      let __src_1 := toRingHom G R (x * y);
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝ =
    ((let __src := DistribMulAction.toAddEquiv R x;
        let __src_1 := toRingHom G R x;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }) *
        let __src := DistribMulAction.toAddEquiv R y;
        let __src_1 := toRingHom G R y;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
hp : Irreducible 1
⊢ False

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Monoid M
hp : Irreducible 1
⊢ False
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
x : R
hy : e x ∈ s
⊢ ↑e.symm (e x) ∈ s'

Tactic:
;

Goal state after:
R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
x : R
hy : e x ∈ s
⊢ ↑e.symm (e x) ∈ s'
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
← u.isUnit_mul_units B

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑u)
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Monoid N
f : F
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
inst✝ : IsLocalHom f
p q : M
hfx : Irreducible (f (p * q))
⊢ IsUnit p ∨ IsUnit q

Tactic:
;

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Monoid N
f : F
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
inst✝ : IsLocalHom f
p q : M
hfx : Irreducible (f (p * q))
⊢ IsUnit p ∨ IsUnit q
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
S : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : SetLike S M₀
inst✝ : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : ↑x = 0
⊢ ↑x = ↑(x * x)

Tactic:
;

Goal state after:
M₀ : Type u_1
S : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : SetLike S M₀
inst✝ : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : ↑x = 0
⊢ ↑x = ↑(x * x)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
x : M₀
⊢ x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * ↑d)

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * ↑d)