mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ b ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ b ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
i✝ : l
j✝ : p
⊢ (M.submatrix e₁ id * N.submatrix (⇑e₂) id) i✝ j✝ = (M.submatrix e₁ ⇑e₂.symm * N) i✝ j✝

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
i✝ : l
j✝ : p
⊢ (M.submatrix e₁ id * N.submatrix (⇑e₂) id) i✝ j✝ = (M.submatrix e₁ ⇑e₂.symm * N) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
i✝ : m
j✝ : l
⊢ (M.submatrix id ⇑e₂ * N.submatrix id e₁) i✝ j✝ = (M * N.submatrix (⇑e₂.symm) e₁) i✝ j✝

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
i✝ : m
j✝ : l
⊢ (M.submatrix id ⇑e₂ * N.submatrix id e₁) i✝ j✝ = (M * N.submatrix (⇑e₂.symm) e₁) i✝ j✝
Module: Mathlib.Order.Preorder.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : Lattice M
f g : ι →₀ M
inst✝ : DecidableEq ι
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : Lattice M
f g : ι →₀ M
inst✝ : DecidableEq ι
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑⟨x, hx✝⟩ ∈ S i
⊢ iUnionLift S f hf T hT ⟨x, hx✝⟩ = f i ⟨↑⟨x, hx✝⟩, hx⟩

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑⟨x, hx✝⟩ ∈ S i
⊢ iUnionLift S f hf T hT ⟨x, hx✝⟩ = f i ⟨↑⟨x, hx✝⟩, hx⟩
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ 0 • {a} = 0

Tactic:
;

Goal state after:
α : Type u_1
a : α
n : ℕ
⊢ 0 • {a} = 0
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
x✝ : α
⊢ x✝ ∈ (fun a ↦ ⟨a, ⋯⟩) ⁻¹' inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t ↔ x✝ ∈ ⋃ i, Subtype.val '' f i ⁻¹' t

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
x✝ : α
⊢ x✝ ∈ (fun a ↦ ⟨a, ⋯⟩) ⁻¹' inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t ↔ x✝ ∈ ⋃ i, Subtype.val '' f i ⁻¹' t
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n ↦ n • {a}) = f.sum fun x n ↦ Multiset.count a (n • {x})

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n ↦ n • {a}) = f.sum fun x n ↦ Multiset.count a (n • {x})
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
x : Matrix n n α
i✝ j✝ : n
⊢ (r • x) i✝ j✝ = (((scalar n).comp (algebraMap R α)) r * x) i✝ j✝

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
x : Matrix n n α
i✝ j✝ : n
⊢ (r • x) i✝ j✝ = (((scalar n).comp (algebraMap R α)) r * x) i✝ j✝
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ (toFinsupp {a}) a✝ = (Finsupp.single a 1) a✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ (toFinsupp {a}) a✝ = (Finsupp.single a 1) a✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
i✝ j✝ : m
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) i✝ j✝ = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop)) i✝ j✝

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
i✝ j✝ : m
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) i✝ j✝ = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop)) i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
i✝ j✝ : Fin n
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) i✝ j✝ =
    ({ toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
        { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝)
      i✝ j✝

Tactic:
;

Goal state after:
α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
i✝ j✝ : Fin n
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) i✝ j✝ =
    ({ toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
        { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝)
      i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring α
inst✝⁴ : Semiring β
inst✝³ : Semiring γ
inst✝² : Algebra R α
inst✝¹ : Algebra R β
inst✝ : Algebra R γ
x✝ : R
i✝ j✝ : m
⊢ MulOpposite.unop (RingEquiv.mopMatrix.toFun ((algebraMap R (Matrix m m αᵐᵒᵖ)) x✝)) i✝ j✝ =
    MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ) x✝) i✝ j✝

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring α
inst✝⁴ : Semiring β
inst✝³ : Semiring γ
inst✝² : Algebra R α
inst✝¹ : Algebra R β
inst✝ : Algebra R γ
x✝ : R
i✝ j✝ : m
⊢ MulOpposite.unop (RingEquiv.mopMatrix.toFun ((algebraMap R (Matrix m m αᵐᵒᵖ)) x✝)) i✝ j✝ =
    MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ) x✝) i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring α
inst✝⁴ : Semiring β
inst✝³ : Semiring γ
inst✝² : Algebra R α
inst✝¹ : Algebra R β
inst✝ : Algebra R γ
x✝ : R
⊢ MulOpposite.unop (RingEquiv.mopMatrix.toFun ((algebraMap R (Matrix m m αᵐᵒᵖ)) x✝)) =
    MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ) x✝)

Tactic:
ext; simp [algebraMap_matrix_apply, eq_comm, apply_ite MulOpposite.unop]

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β✝ : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → Mul (β i)
inst✝ : Fintype n
x✝² x✝¹ : Matrix n n ((i : ι) → β i)
x✝ : ι
i✝ j✝ : n
⊢ piAddEquiv.toFun (x✝² * x✝¹) x✝ i✝ j✝ = (piAddEquiv.toFun x✝² * piAddEquiv.toFun x✝¹) x✝ i✝ j✝

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β✝ : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → Mul (β i)
inst✝ : Fintype n
x✝² x✝¹ : Matrix n n ((i : ι) → β i)
x✝ : ι
i✝ j✝ : n
⊢ piAddEquiv.toFun (x✝² * x✝¹) x✝ i✝ j✝ = (piAddEquiv.toFun x✝² * piAddEquiv.toFun x✝¹) x✝ i✝ j✝
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : M}, c x y → d x y

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : M}, c x y → d x y
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : R}, c x y → d x y

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : R}, c x y → d x y
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : Module.rank R M = 0
⊢ Subsingleton M

Tactic:
rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
  exact (Module.Free.chooseBasis R M).repr.subsingleton

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
I✝ : TwoSidedIdeal R
inst✝ : Nontrivial R
I J : RingCon R
h : { ringCon := I } = { ringCon := J }
⊢ I = J

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
I✝ : TwoSidedIdeal R
inst✝ : Nontrivial R
I J : RingCon R
h : { ringCon := I } = { ringCon := J }
⊢ I = J
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ I.ringCon (x - y) 0

Tactic:
;

Goal state after:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ I.ringCon (x - y) 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ 0 = y - y

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon x y
⊢ 0 = y - y
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ I.ringCon x y

Tactic:
;

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ I.ringCon x y
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ x - y ∈ I

Tactic:
by
  rw [mem_iff]
  constructor
  · intro h; convert! I.ringCon.sub h (I.ringCon.refl y); abel
  · intro h; convert! I.ringCon.add h (I.ringCon.refl y) <;> abel

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h : ↑I ⊆ ↑J
x y : R
r : x - y ∈ { ringCon := { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I }
⊢ x - y ∈ { ringCon := { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J }

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h : ↑I ⊆ ↑J
x y : R
r : x - y ∈ { ringCon := { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I }
⊢ x - y ∈ { ringCon := { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J }
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : I.ringCon x 0
⊢ J.ringCon x 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : I.ringCon x 0
⊢ J.ringCon x 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x : RingCon R
⊢ { ringCon := x } = { ringCon := { ringCon := x }.ringCon }

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x : RingCon R
⊢ { ringCon := x } = { ringCon := { ringCon := x }.ringCon }
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d = a * c - a * d + (a * d - b * d)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d = a * c - a * d + (a * d - b * d)
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ K.ringCon
h2 : J.ringCon ≤ K.ringCon
⊢ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon ≤ K.ringCon

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ K.ringCon
h2 : J.ringCon ≤ K.ringCon
⊢ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon ≤ K.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
a : R
ha : a ∈ I
b : R
hb : b ∈ J
⊢ x + y + (a + b) ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
a : R
ha : a ∈ I
b : R
hb : b ∈ J
⊢ x + y + (a + b) ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ * y) = f (x * z)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ * y) = f (x * z)
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ + y) = f (x + z)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ + y) = f (x + z)
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ ∃ y ∈ I, ∃ z ∈ J, y + z = x
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ s.ringCon x 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ s.ringCon x 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
x✝ : M
⊢ ((c + d) • LinearMap.id) x✝ = (c • LinearMap.id + d • LinearMap.id) x✝

Tactic:
;

Goal state after:
R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
x✝ : M
⊢ ((c + d) • LinearMap.id) x✝ = (c • LinearMap.id + d • LinearMap.id) x✝
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
x✝ : M
⊢ ((c • d) • LinearMap.id) x✝ = ((RingHom.id R) c • d • LinearMap.id) x✝

Tactic:
;

Goal state after:
R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
x✝ : M
⊢ ((c • d) • LinearMap.id) x✝ = ((RingHom.id R) c • d • LinearMap.id) x✝
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : NonAssocRing A
inst✝ : IsSimpleRing A
x : A
hx : x ≠ 0
hxI : x ∈ ⊥
⊢ False

Tactic:
;

Goal state after:
A : Type u_2
inst✝¹ : NonAssocRing A
inst✝ : IsSimpleRing A
x : A
hx : x ≠ 0
hxI : x ∈ ⊥
⊢ False