mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (lTensorHom M) (f - g) = (lTensorHom M) f - (lTensorHom M) g

Tactic:
exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y ∈ a, ∃ a, a • y = x) ↔ x ∈ a

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y ∈ a, ∃ a, a • y = x) → x ∈ a

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a → ∃ y ∈ a, ∃ a, a • y = x
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: m n : ℤ
⊢ IsCoprime m n ↔ m.gcd n = 1

Tactic:
constructor

Goal state after:
case mp
m n : ℤ
⊢ IsCoprime m n → m.gcd n = 1

case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
constructor

Goal state after:
case cons.mp
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) →
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

case cons.mpr
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)) →
    ∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap 1 = 1

Tactic:
ext

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map f.toLinearMap 1 ↔ x✝ ∈ 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ comap (↑(opLinearEquiv R)) 1 = 1

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 1 ↔ x✝ ∈ 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ↔
    S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) →
    S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

case mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) →
    S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ =
    (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y

Tactic:
ext

Goal state after:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy : (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y = S
x✝ : A'
⊢ x✝ ∈ (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) ⟨f ↑y, ⋯⟩ ↔
    x✝ ∈ (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
⊢ ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a

Tactic:
rw [← mul_sum, ← sum_mul, hμ, one_mul]

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : f y' = ↑y
⊢ (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ =
    (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y

Tactic:
ext

Goal state after:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : f y' = ↑y
x✝ : A'
⊢ x✝ ∈ (fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ⟨y', hy'⟩ ↔
    x✝ ∈ (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * (μ x * ∏ j ∈ insert a t \ {x}, s j)) =
    v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
if_neg fun ha : x = a ↦ hat (ha.casesOn hx)

Goal state after:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p ↔ x⁻¹ * y ∈ p

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p → x⁻¹ * y ∈ p

case mpr
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ x⁻¹ * y ∈ p → y ∈ x • p
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ ≤ ⊤ * P

Tactic:
conv_lhs => rw [← mul_one ⊤, ← h, ← mul_assoc]
    exact smul_mono_left le_top

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ MonoidHom.mker (spanSingleton R) = Submonoid.map (algebraMap R A) (IsUnit.submonoid R)

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ x✝ ∈ Submonoid.map (algebraMap R A) (IsUnit.submonoid R)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ (Units.map ↑(spanSingleton R)).ker = (Units.map ↑(algebraMap R A)).range

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : Aˣ
⊢ x✝ ∈ (Units.map ↑(spanSingleton R)).ker ↔ x✝ ∈ (Units.map ↑(algebraMap R A)).range
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h y = x) ↔ ∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h y = x) → ∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y

case mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y) → ∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h y = x
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ I.IsPrime

Tactic:
constructor

Goal state after:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ I ≠ ⊤

case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ I.IsPrime ↔ (∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p

Tactic:
constructor

Goal state after:
case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ I.IsPrime → (∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p

case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ((∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p) → I.IsPrime
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
⊢ Injective ⇑f

Tactic:
let f' := j.symm.toLinearMap ∘ₗ f ∘ₗ (LinearEquiv.ofInjective i' hi).symm.toLinearMap

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
⊢ Injective ⇑f
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case inr
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update 0 i r * x + update 1 i y) j

Tactic:
· simp [update_of_ne ne]

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a = 0
⊢ b = gcd (b % a) a

Tactic:
simp only [h, mod_zero, gcd_zero_right]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I ↔ ∃ x ∈ I, e x = y

Tactic:
constructor

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I → ∃ x ∈ I, e x = y

case mpr
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ (∃ x ∈ I, e x = y) → y ∈ map e I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

Tactic:
constructor

Goal state after:
case mp
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

case mpr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) → x ∈ I • span R (Set.range f)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K.radical = (comap f K).radical

Tactic:
ext

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
x✝ : R
⊢ x✝ ∈ comap f K.radical ↔ x✝ ∈ (comap f K).radical
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
⊢ ker ↑f = ⊥

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R ≃+* S
x✝ : R
⊢ x✝ ∈ ker ↑f ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
F' : Type u_3
inst✝¹ : EquivLike F' R S
inst✝ : RingEquivClass F' R S
f : F'
⊢ ker f = ⊥

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
F' : Type u_3
inst✝¹ : EquivLike F' R S
inst✝ : RingEquivClass F' R S
f : F'
x✝ : R
⊢ x✝ ∈ ker f ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M = ⊥ ↔ FaithfulSMul R M

Tactic:
rw [← le_bot_iff]
  refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩
  · rw [← sub_eq_zero]
    exact H (Module.mem_annihilator (r := r - s).mpr
      (by simp only [sub_smul, H', sub_self, implies_true]))
  · exact @H a 0 (by simp [Module.mem_annihilator.mp ha])

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 → x = 0 ∨ y = 0

case mpr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ x = 0 ∨ y = 0 → lcm x y = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
⊢ annihilator R (M × M') = annihilator R M ⊓ annihilator R M'

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ x✝ ∈ annihilator R (M × M') ↔ x✝ ∈ annihilator R M ⊓ annihilator R M'
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : ι →₀ M), r • m = 0) ↔ ∀ (m : M), r • m = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : ι →₀ M), r • m = 0) → ∀ (m : M), r • m = 0

case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : M), r • m = 0) → ∀ (m : ι →₀ M), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0

case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : Π₀ (i : ι), M i), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ annihilator R (Π₀ (i : ι), M i) = ⨅ i, annihilator R (M i)

Tactic:
ext r; simp only [mem_annihilator, Ideal.mem_iInf]
  constructor <;> intro h
  · intro i m
    classical simpa using DFunLike.congr_fun (h (DFinsupp.single i m)) i
  · intro m; ext i; exact h i _

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : (i : ι) → M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0

case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : (i : ι) → M i), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) ↔ ∀ (n : ↑s), r • ↑n = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) → ∀ (n : ↑s), r • ↑n = 0

case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ n ∈ span R s, r • n = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).annihilator = ⨅ g, (toSpanSingleton R M ↑g).ker

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : R
⊢ x✝ ∈ (span R s).annihilator ↔ x✝ ∈ ⨅ g, (toSpanSingleton R M ↑g).ker
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (a ∣ s.gcd ↔ ∀ (b : α), b ∈ s → a ∣ b) → (a ∣ (a_1 ::ₘ s).gcd ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ∣ b)

Tactic:
simp +contextual [or_imp, forall_and, dvd_gcd_iff]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0

case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0