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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
⊢ a * b = a0 * b0 → a = a0 ∧ b = b0

Tactic:
ab

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ f (a * b) = f (a0 * b0)

Tactic:
ab

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter

Goal state after:
case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n

case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]
  rfl

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
simp [pow_succ, product_pow _ _ n]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
ih : (monomial n) r ^ k = (monomial (n * k)) (r ^ k)
⊢ (monomial n) r ^ (k + 1) = (monomial (n * (k + 1))) (r ^ (k + 1))

Tactic:
simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).toFinsupp = AddMonoidAlgebra.erase n p.toFinsupp

Tactic:
by
  simp only [erase_def]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[ℕ]
n : ℕ
⊢ { toFinsupp := AddMonoidAlgebra.erase n p } = erase n { toFinsupp := p }

Tactic:
by
  simp only [erase_def]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.coeff n ≠ 0
⊢ p.coeffs.Nonempty

Tactic:
exact ⟨p.coeff n, coeff_mem_coeffs hn⟩

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
⊢ UniqueProds (G × H)

Tactic:
refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he => Prod.ext ?_ ?_)
      (UniqueProds.instForall <| I G H) <;> apply up_injective
    exacts [congr_fun he false, congr_fun he true]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
this : ∃ l ∈ supported R R ↑t1, (linearCombination R id) l = f x
⊢ x ∈ span R (g '' ↑t1) ⊔ span R ↑t2

Tactic:
rcases this with ⟨l, hl1, hl2⟩

Goal state after:
case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ x ∈ span R (g '' ↑t1) ⊔ span R ↑t2
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ height x ≤ height (f x)

Tactic:
simp only [height_eq_iSup_last_eq]
  apply iSup₂_le
  intro p hlast
  apply le_iSup₂_of_le (p.map f hf) (by simp [hlast]) (by simp)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 2
⊢ ∃ y, ∃ z < y, y < x

Tactic:
refine ⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩ <;> simp [Fin.lt_def, hlen]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : α), ↑(height i) ≤ krullDim α

Tactic:
apply height_le_krullDim

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ coheight x < ⊤

Tactic:
rw [← WithBot.coe_lt_coe]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ ↑(coheight x) < ↑⊤
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'₂ : Type u_22
inst✝³ : Monoid R'₂
inst✝² : DistribMulAction R'₂ M
inst✝¹ : SMulCommClass R R'₂ M
inst✝ : SMulCommClass R' R'₂ M
r' : R'
r'₂ : R'₂
x✝ x y : M ⊗[R] N
ihx : r' • r'₂ • x = r'₂ • r' • x
ihy : r' • r'₂ • y = r'₂ • r' • y
⊢ r' • r'₂ • (x + y) = r'₂ • r' • (x + y)

Tactic:
by
      simp_rw [TensorProduct.smul_add]; rw [ihx, ihy]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n✝ n : ℕ
⊢ mulRight R a ^ (n + 1) = mulRight R (a ^ (n + 1))

Tactic:
by rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]

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

Goal state before:
pp: m n : ℕ
⊢ IsCoprime m n ↔ m = 1 ∨ n = 1

Tactic:
refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩
  · simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H
    exact H.symm.imp (·.1.2) (·.2.2)
  · obtain rfl | rfl := h
    · exact isCoprime_one_left
    · exact isCoprime_one_right

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

Goal state before:
pp: case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n

Tactic:
· rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
    intro h
    exact ⟨_, _, h⟩

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

Goal state before:
pp: A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Semiring C
inst✝⁵ : SMul A B
inst✝⁴ : Module A C
inst✝³ : Module B C
inst✝² : IsScalarTower A C C
inst✝¹ : IsScalarTower B C C
inst✝ : IsScalarTower A B C
I : Submodule B C
n : ℕ
x✝ : n + 2 ≠ 0
⊢ restrictScalars A (I ^ (n + 2)) = restrictScalars A I ^ (n + 2)

Tactic:
by
    simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]

Goal state after:
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
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)

Tactic:
refine Finset.induction_on s ?_ ?_

Goal state after:
case refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ ∅, span R (M i) = span R (∏ i ∈ ∅, M i)

case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i) → ∏ i ∈ insert a s, span R (M i) = span R (∏ i ∈ insert a s, M i)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
inst✝ : Finite M
s : Submodule R M
⊢ Submodule.span R ↑⋯.toFinset = s

Tactic:
rw [Set.Finite.coe_toFinset, Submodule.span_eq]

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
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ (LinearMap.toSpanSingleton R M x).range ≤ M'

Tactic:
rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ s ⊆ ↑(comap (LinearMap.toSpanSingleton R M x) M')
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

Tactic:
rintro x y - - ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩

Goal state after:
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)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = (ax.sum fun i c ↦ c • f i) + ay.sum fun i c ↦ c • f i
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map (fun x ↦ s.gcd * x) t
⊢ t.gcd = 1

Tactic:
rw [← normalize_gcd, normalize_eq_one, ← associated_one_iff_isUnit]
  refine .of_mul_left (.symm ?_) .rfl (a := s.gcd) ?_
  · simpa using (Associated.of_eq <| congr(gcd $ht)).trans (associated_gcd_map_mul ..)
  contrapose! hs
  exact s.gcd_eq_zero_iff.1 hs

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i

Tactic:
refine Finset.induction_on s ?_ ?_

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: z : ℤ
hz : normalize z = z
⊢ 0 ≤ z

Tactic:
by
  by_cases! h : 0 ≤ z
  · exact h
  · rw [normalize_of_nonpos h.le] at hz
    lia

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).gcd f = GCDMonoid.gcd (s.gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = GCDMonoid.gcd ((insert a s).gcd f) (s₂.gcd f)

Tactic:
by rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = ⊤
⊢ I + ⨅ j ∈ s, J j = ⊤

Tactic:
exact sup_iInf_eq_top hf

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = b - a * d

Tactic:
← hd,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = b - (b - c)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = c + a * d

Tactic:
← hd,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = c + (b - c)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y

Tactic:
← Ideal.span_singleton_le_span_singleton

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y z : R
inst✝ : IsPrincipal (Ideal.span {x, y})
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, A + b = 0 ∧ b + A = 0) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0

Tactic:
← Matrix.ext_iff,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), (A + b) i j = 0 i j) ∧ ∀ (i : m) (j : n), (b + A) i j = 0 i j) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0
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 u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Finite ↑w
s : range v ⊆ ↑(span R w)
this : Fintype ↑w := Fintype.ofFinite ↑w
t : Finset ι
v' : ↑↑t → M := fun x ↦ v ↑x
i' : LinearIndependent (ι := ↑↑t) R v'
⊢ t.card ≤ Fintype.card ↑w

Tactic:
have s' : range v' ≤ span R w := (range_comp_subset_range _ _).trans s

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Finite ↑w
s : range v ⊆ ↑(span R w)
this : Fintype ↑w := Fintype.ofFinite ↑w
t : Finset ι
v' : ↑↑t → M := fun x ↦ v ↑x
i' : LinearIndependent (ι := ↑↑t) R v'
s' : range v' ⊆ ↑(span R w)
⊢ t.card ≤ Fintype.card ↑w
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
| ∀ (i j : n), (if i = j then d i else 0) ∈ S

Tactic:
intro _ _

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (if i✝ = j✝ then d i✝ else 0) ∈ S
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 u_2
v : ι → M
i : LinearIndependent R v
w : Finset M
s : span R ↑w = ⊤
⊢ #ι ≤ ↑w.card

Tactic:
by
  simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s

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
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k ↦ v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {Φ p})) R v'
⊢ v' ⟨p, ⋯⟩ ∈ span R (⇑b '' ↑(Φ p))

Tactic:
apply Basis.mem_span_repr_support

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
| ∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S

Tactic:
intro _ _

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (if i = i✝ ∧ j = j✝ then a else 0) ∈ S
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 α
h : ∀ (i : m), Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N
⊢ M = N

Tactic:
by
  ext i j
  simp_rw [single_one_vecMul] at h
  exact congrFun (h i) j

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

Goal state before:
pp: case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a

Tactic:
· exact Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R},
    x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} →
      y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x + y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩

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

Goal state before:
pp: ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
rw [AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, AddMonoidHom.mrange_eq_top]

Goal state after:
ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Surjective ⇑(DFinsupp.sumAddHom fun i ↦ (A i).subtype)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ : Subalgebra R A
S : Subalgebra R R
⊢ S ≤ default

Tactic:
intro _ _

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ : Subalgebra R A
S : Subalgebra R R
x✝ : R
a✝ : x✝ ∈ S
⊢ x✝ ∈ default
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) (-↑i) ∈ S.carrier
⊢ ↑(-↑i) - ↑1 ∈ S

Tactic:
Int.cast_one

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) (-↑i) ∈ S.carrier
⊢ ↑(-↑i) - 1 ∈ S
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ y

Tactic:
by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
          all_goals simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
s : Set A
x : A
⊢ x ∈ adjoin R s ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)

Tactic:
rw [← Subalgebra.mem_toSubring, adjoin_eq_ring_closure]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j

Tactic:
rcases i with ⟨⟩

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : n
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝) j = M (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : o
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝) j = M (Sum.inr val✝) j