mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

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

Tactic:
apply le_antisymm

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

case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀

Tactic:
cases nonempty_fintype α
  simpa using exists_max_image univ f univ_nonempty

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

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

Tactic:
by rw [one_mul, zero_mul, zero_add]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_left

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x

Tactic:
exact h.of_add_mul_left_left

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime (y + x * z) x
⊢ IsRelPrime y x

Tactic:
exact h.of_add_mul_left_left

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
P : Submodule R A
⊢ 1 ≤ P ↔ 1 ∈ P

Tactic:
simp [one_eq_span]

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

Goal state before:
pp: case neg
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 → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : ¬x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

Tactic:
Pi.single_eq_of_ne hx,

Goal state after:
case neg
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 → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : ¬x = Exists.choose h
⊢ 0 = Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case neg
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 → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : ¬x = Exists.choose h
⊢ 0 = Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

Tactic:
Pi.single_eq_of_ne hx,

Goal state after:
case neg
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 → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : ¬x = Exists.choose h
⊢ 0 = 0 * ∏ j ∈ t \ {x}, s j
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
⊢ map (↑(opLinearEquiv R)) (M * N) = map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) (M * N) ≤ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M

case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a : K
ha : a ≠ 0
b : K
⊢ EuclideanDomain.gcd a b = a

Tactic:
by
  rw [Field.gcd_eq, if_neg ha]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0

Tactic:
exact dvd_zero _

Goal state after:
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
m x : M
hx : x ∈ I • (R ∙ m)
m1 m2 : M
x✝¹ : ∃ y ∈ I, y • m = m1
x✝ : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ m1 + y2 • m = m1 + m2

Tactic:
hy2

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
m x : M
hx : x ∈ I • (R ∙ m)
m1 m2 : M
x✝¹ : ∃ y ∈ I, y • m = m1
x✝ : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ m1 + m2 = m1 + m2
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁷ : Semiring R✝
inst✝⁶ : Semiring S
inst✝⁵ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝⁴ : FunLike G S R✝
inst✝³ : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝² : (i : ι) → Semiring (R i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal I

Tactic:
rw [← piOrderIso.symm_apply_apply I]

Goal state after:
R✝ : Type u
S : Type v
F : Type u_1
inst✝⁷ : Semiring R✝
inst✝⁶ : Semiring S
inst✝⁵ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝⁴ : FunLike G S R✝
inst✝³ : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝² : (i : ι) → Semiring (R i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal (piOrderIso.symm (piOrderIso I))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : J ⊔ comap f ⊥ = ⊤
⊢ J = ⊤

Tactic:
eq_top_iff

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤

Tactic:
eq_top_iff

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ ⊤ ≤ J
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0

Tactic:
exact dvd_zero _

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

Goal state before:
pp: case mp.refine_3
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
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    x ∈ span R (↑I • Set.range f) →
      y ∈ span R (↑I • Set.range f) →
        (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
          (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = y) →
            ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x + y

pp: case mp.refine_4
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
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (↑I • Set.range f),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c ↦ c • f i) = a • x

Tactic:
· rintro x y - - ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩
    refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩ <;>
      intros <;> simp only [zero_smul, add_smul]

Goal state after:
case mp.refine_4
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
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (↑I • Set.range f),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c ↦ c • f i) = a • x
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0

Tactic:
exact dvd_zero _

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

Goal state before:
pp: case mp.refine_4
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
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ((c • a).sum fun i c ↦ c • f i) = c • a.sum fun i c ↦ c • f i

Tactic:
rw [Finsupp.sum_smul_index, Finsupp.smul_sum]

Goal state after:
case mp.refine_4
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
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

case mp.refine_4
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
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (i : ι), 0 • f i = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m ≤ n
⊢ I ^ n ≤ I ^ m

Tactic:
obtain _ | m := m

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0

case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
h : m + 1 ≤ n
⊢ I ^ n ≤ I ^ (m + 1)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ 1

Tactic:
one_eq_top

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ IsTwoSided 1

Tactic:
one_eq_top

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ ⊤.IsTwoSided
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
N P : Submodule R M
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
by
  rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ 1 = ⊤

Tactic:
one_eq_top

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ 1 = ⊤

Tactic:
one_eq_top

Goal state after:
case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case refine_2
n : ℕ
⊢ |↑n|.natAbs = n

Tactic:
Int.natAbs_abs,

Goal state after:
case refine_2
n : ℕ
⊢ (↑n).natAbs = n
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = GCDMonoid.gcd 0 ({x ∈ s | f x ≠ 0}.gcd f)

Tactic:
refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)

Goal state after:
case refine_2.refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ {x ∈ ∅ | f x = 0}.gcd f = 0

case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ∀ (a : β) (s : Finset β), a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ ↔ I ⊔ J = 1

Tactic:
one_eq_top

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
⊢ 1 * ↑(Units.mkOfMulEqOne a b h) = a

Tactic:
Units.val_mkOfMulEqOne,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
⊢ 1 * a = a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
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₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
⊢ d₁ ^ k * ↑(Units.mkOfMulEqOne a' b' h') = a

Tactic:
Units.val_mkOfMulEqOne,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
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₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
⊢ d₁ ^ k * a' = a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ IsUnit (gcd x y)

Tactic:
← normalize_eq_one,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ normalize (gcd x y) = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : 1 ≤ P
hn : n = 0
⊢ I ≤ P

Tactic:
one_eq_top

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : ⊤ ≤ P
hn : n = 0
⊢ I ≤ P
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: R : Type u_7
inst✝ : Zero R
m n : ℕ
A : Array R
hA : A.size = m * n
i : Fin m
j : Fin n
⊢ ofArray A hA i j = of (fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j

Tactic:
have : n * i.val + j.val < m * n := (Fin.mkDivMod i j).isLt

Goal state after:
R : Type u_7
inst✝ : Zero R
m n : ℕ
A : Array R
hA : A.size = m * n
i : Fin m
j : Fin n
this : n * ↑i + ↑j < m * n
⊢ ofArray A hA i j = of (fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
S : Set α
x✝ : Matrix m n α
⊢ x✝ ∈ S.matrix ↔ x✝ ∈ ⇑of.symm ⁻¹' univ.pi fun x ↦ univ.pi fun x ↦ S

Tactic:
simp [Set.mem_matrix]

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

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
b✝ : Associates α
b : α
⊢ Quotient.map₂ gcd ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) ∣
    Quot.mk (⇑(Associated.setoid α)) b

Tactic:
exact mk_le_mk_of_dvd (gcd_dvd_right _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j)
⊢ b ∈ ⋃ j, S' j

Tactic:
v.repr_self,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : Finsupp.single i 1 ∈ Finsupp.supported R R (⋃ j, S j)
⊢ b ∈ ⋃ j, S' j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ = #ι

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ ≤ #ι

case a
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #ι ≤ #κ
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι = ⨆ ι, #↑↑ι

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤ ⨆ ι, #↑↑ι

case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ⨆ ι, #↑↑ι ≤ #ι
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R {x | x ∈ s}) = #↑{x | x ∈ s}

Tactic:
← Subtype.range_coe_subtype

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R (range Subtype.val)) = #↑(range Subtype.val)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i
aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x, ∃ (_ : x ∈ s), I ≤ f x
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
exists_prop

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x ∈ s, I ≤ f x
⊢ ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M + -M') * N = M * N - M' * N

Tactic:
Matrix.add_mul,

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ M * N + -M' * N = M * N - M' * N
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x, ∑ i, v x * (A x i * w i) = ∑ x, ∑ x_1, v x_1 * (A x_1 x * w x)

Tactic:
exact Finset.sum_comm

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
⊢ (single i i c).diag j = Pi.single i c j

Tactic:
by_cases hij : i = j

Goal state after:
case pos
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single i i c).diag j = Pi.single i c j

case neg
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : ¬i = j
⊢ (single i i c).diag j = Pi.single i c j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ ⊤ = 1

Tactic:
one_eq_top

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ ⊤ = ⊤
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), Commute (single i j 1) M

Tactic:
by
  refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
    fun hM => mem_range_scalar_iff_commute_single.mpr <| fun i j _ => hM i j⟩
  rw [scalar_commute_iff]
  simp

Goal state after: