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

Goal state before:
pp: case refine_1.left
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Injective ⇑((↑l).prod g)

pp: case refine_1.right
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑((↑l).prod g)

Tactic:
· intro x y e
      simp only [LinearMap.prod_apply, Function.prod_apply, Prod.mk.injEq] at e
      obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
      rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]

Goal state after:
case refine_1.right
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑((↑l).prod g)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1.right
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x : M
y : N
⊢ ∃ a, ((↑l).prod g) a = (x, g y)

Tactic:
refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩

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

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹² : Monoid R
inst✝¹¹ : Monoid S
inst✝¹⁰ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : DistribMulAction R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : DistribMulAction S B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝³ : NonUnitalNonAssocSemiring B₁
inst✝² : DistribMulAction R B₁
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
x y : A
⊢ Function.prod (⇑f) (⇑g) (x + y) = Function.prod (⇑f) (⇑g) x + Function.prod (⇑f) (⇑g) y

Tactic:
by simp only [Function.prod_apply, Prod.mk_add_mk, map_add]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x

Tactic:
simp only [RelSeries.snoc_length, RelSeries.eraseLast_length, Nat.cast_add, ENat.natCast_sub,
        Nat.cast_one, p'] at this

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ ↑p.length ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ height x ≤ ↑n ↔ ∀ y < x, height y < ↑n

Tactic:
conv_lhs => rw [height_eq_iSup_lt_height, iSup₂_le_iff]
  congr! 2 with y _
  cases height y
  · simp
  · norm_cast

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
n : N
⊢ (SMul.aux r) (FreeAddMonoid.of (0, n)) = (SMul.aux r) 0

Tactic:
by simp_rw [map_zero, SMul.aux_of, smul_zero, zero_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x p q : M ⊗[R] N
ih1 : (liftAux f') (r • p) = σ₁₂ r • (liftAux f') p
ih2 : (liftAux f') (r • q) = σ₁₂ r • (liftAux f') q
⊢ (liftAux f') (r • p) + (liftAux f') (r • q) = σ₁₂ r • ((liftAux f') p + (liftAux f') q)

Tactic:
ih1,

Goal state after:
R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x p q : M ⊗[R] N
ih1 : (liftAux f') (r • p) = σ₁₂ r • (liftAux f') p
ih2 : (liftAux f') (r • q) = σ₁₂ r • (liftAux f') q
⊢ σ₁₂ r • (liftAux f') p + (liftAux f') (r • q) = σ₁₂ r • ((liftAux f') p + (liftAux f') q)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
n : ℕ
⊢ height ↑n = ↑n

Tactic:
exact (height_coe_withTop _).trans (height_nat _)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ lift (lsmul R M ∘ₗ (mul R R) r) = (lsmul R M) r ∘ₗ lift (lsmul R M)

Tactic:
by
  apply TensorProduct.ext'
  intro x a
  simp [← mul_smul, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f✝ : N →ₗ[R] P
r : R
f : N →ₗ[R] P
x : N
y : M
⊢ (((TensorProduct.mk R N M).compr₂ₛₗ (rTensor M (r • f))) x) y =
    (((TensorProduct.mk R N M).compr₂ₛₗ (r • rTensor M f)) x) y

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, smul_tmul, tmul_smul, smul_apply, rTensor_tmul]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T

Tactic:
rw [closure_le]

Goal state after:
case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 * x = 1

Tactic:
by rwa [zero_mul, add_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')

Tactic:
obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx
  obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h
  use T, T', hS, hS'
  have h' : (U : Set A) ⊆ T * T' := by assumption_mod_cast
  have h'' := span_mono h' hU
  assumption

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
P Q : Submodule R A
x : A
hx : x ∈ P * Q
⊢ x ∈ span R (↑P * ↑Q)

Tactic:
rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : (↑t).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsCoprime (s i) (s j)

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj

Goal state after:
case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : (↑t).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i ↦ s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsRelPrime (s i) (s j)

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj

Goal state after:
case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i ↦ s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsRelPrime (s i) (s j)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
s : Submodule R M
f : M →ₛₗ[σ] P
inst✝ : IsNoetherian R ↥s
⊢ (f.submoduleMap s).range = ⊤

Tactic:
simp [LinearMap.submoduleMap]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ s ⊆ ⇑f ⁻¹' ↑(Submodule.span S (⇑f '' s))

Tactic:
← Set.image_subset_iff

Goal state after:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ ⇑f '' s ⊆ ↑(Submodule.span S (⇑f '' s))
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
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝² x✝¹ : R
x✝ : x✝¹ ∈ span R S
h : x✝¹ • m ∈ span R (S • T)
⊢ (x✝² • x✝¹) • m ∈ span R (S • T)

Tactic:
by rw [smul_assoc]; exact smul_mem _ _ h

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
xgcdAux_val,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : P a b (gcd a b, xgcd a b)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case zero
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 ^ 0 ≤ comap f (K ^ 0)

Tactic:
rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
    exact rfl.le

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : comap f (map f I) = comap f ⊤
⊢ ⊤ ≤ I

Tactic:
rw [comap_map_of_surjective _ hf, comap_top] at h

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z

Tactic:
rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]

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

Goal state before:
pp: a b : ℤ
⊢ Associated (↑(a.gcd b) * ↑(a.lcm b)) (a * b)

Tactic:
rw [← Int.natCast_mul, gcd_mul_lcm, ← natAbs_mul, natCast_natAbs, abs_eq_normalize]

Goal state after:
a b : ℤ
⊢ Associated (normalize (a * b)) (a * b)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ comap f I
hx' : f x' = x
⊢ ∃ y ∈ J, f y = x

Tactic:
eq

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : f x' = x
⊢ ∃ y ∈ J, f y = x
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
b : β
hb : b ∈ s
⊢ f b = s.gcd f * (fun x ↦ 1) b

Tactic:
h b hb,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
b : β
hb : b ∈ s
⊢ 0 = s.gcd f * (fun x ↦ 1) b
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr.hab
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ gcd (a * b) (a * c) ∣ a * gcd b c

Tactic:
eq

Goal state after:
case inr.hab
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ a * d ∣ a * gcd b c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
⊢ ∃ d, Associated (d ^ k) a

Tactic:
use d₁

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
⊢ Associated (d₁ ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
⊢ a = 0 ∨ b = 0 → lcm a b = 0

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b : α
⊢ lcm 0 b = 0

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ lcm a 0 = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : c = 0
⊢ a ∣ b

pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : b = 0
⊢ a ∣ c

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
⊢ a ∣ Classical.choose ⋯

Tactic:
· exact ab

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : b = 0
⊢ a ∣ c

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
⊢ a ∣ Classical.choose ⋯
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
⊢ M * 0 = 0

Tactic:
by
  ext
  apply dotProduct_zero

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
j✝ : o
⊢ (L * (M + N)) i✝ j✝ = (L * M + L * N) i✝ j✝

Tactic:
apply dotProduct_add

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝² : NonUnitalNonAssocSemiring β
F : Type u_10
inst✝¹ : FunLike F α β
inst✝ : NonUnitalRingHomClass F α β
f : F
i✝ : m
j✝ : o
⊢ (L * M).map (⇑f) i✝ j✝ = (L.map ⇑f * M.map ⇑f) i✝ j✝

Tactic:
simp [mul_apply, map_sum]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
⊢ 1 * M = M

Tactic:
by
  ext
  rw [← diagonal_one, diagonal_mul, one_mul]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (M * diagonal fun x ↦ 1) i✝ j✝ = M i✝ j✝

Tactic:
mul_diagonal,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M i✝ j✝ * 1 = M i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ (A ^ (m + 1)) i j

Tactic:
rw [pow_succ, mul_apply]

Goal state after:
case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ ∑ j_1, (A ^ m) i j_1 * A j_1 j
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x + y)) x✝ = (A *ᵥ x + A *ᵥ y) x✝

Tactic:
apply dotProduct_add

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
x✝ : n
⊢ (x ᵥ* (A + B)) x✝ = (x ᵥ* A + x ᵥ* B) x✝

Tactic:
apply dotProduct_add

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
i : m
j : n
h : ∀ (i : m), M.row i = N.row i
⊢ M i j = N i j

Tactic:
exact congrFun (h i) j

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #s.toFinset = 1 ↔ s.card ≠ 0 ∧ ∃ a, s = s.card • {a}

Tactic:
simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

Tactic:
induction s using Finset.induction_on <;> simp [*, max_add_add_right]

Goal state after: