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

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
by
      rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
      by_cases hA' : A' = A
      · rw [hA']
        exact ihB B' (hc.2 bi) hB
      · exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB

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

Goal state before:
pp: case a.refine_1
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
⊢ ↑t1 ⊆ g ⁻¹' ↑s

pp: case a.refine_2
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
⊢ ↑t2 ⊆ ↑s

Tactic:
· intro y hy
      exact (hg y hy).1

Goal state after:
case a.refine_2
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
⊢ ↑t2 ⊆ ↑s
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
hx₂ : g' (τ₂ x₂) = 1
⊢ τ₃ (g x₂) = τ₃ 1

Tactic:
by simpa only [map_one, comm₂₃] using hx₂

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

Goal state before:
pp: case refine_2.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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

Tactic:
· rw [LinearEquiv.eq_comp_toLinearMap_symm]
      ext <;> simp [h₁, h₂]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).last = x

Tactic:
by
  simp [singleton, last]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + 1)
⊢ Fin.append p.toFun q.toFun (Fin.cast ⋯ (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i))) = p.toFun i

Tactic:
convert! Fin.append_left _ _ _

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

Goal state before:
pp: G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a : G
⊢ ∀ ⦃b : G⦄, a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0

Tactic:
b

Goal state after:
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
⊢ a ∈ A → b ∈ B → a * b = a0 * b0 → a = a0 ∧ b = b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a : G
⊢ ∀ ⦃b : G⦄, a ∈ A → b ∈ B → a * b = (a1, b1).1 * (a1, b1).2 → a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
b

Goal state after:
case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
⊢ a ∈ A → b ∈ B → a * b = (a1, b1).1 * (a1, b1).2 → a = (a1, b1).1 ∧ b = (a1, b1).2
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ y ∈ t, (f a) y ∈ ↑(map₂ f (span R s) (span R t))

Tactic:
b

Goal state after:
case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
b : N
⊢ b ∈ t → (f a) b ∈ ↑(map₂ f (span R s) (span R t))
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q

Tactic:
rw [← ker_comp, range_liftQ, liftQ_mkQ, ker_comp, range_comp, comap_map_eq,
    ker_mkQ, ker_mkQ, ← hfg.linearMap_ker_eq, sup_comm,
    ← (sup_le hqr (ker_le_comap g)).ge_iff_eq',
    ← comap_map_eq, ← map_le_iff_le_comap, map_comap_eq]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑⊥ ↔ ∀ (l : LTSeries α), l.length < 0

Tactic:
WithBot.lt_coe_bot

Goal state after:
case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length = ⊥ ↔ ∀ (l : LTSeries α), l.length < 0
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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
⊢ lift ((mk R M N).compr₂ₛₗ g) = g

Tactic:
rw [lift_compr₂ₛₗ g, lift_mk, LinearMap.comp_id]

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

Goal state before:
pp: R : Type u_2
inst✝ : AddMonoidWithOne R
⊢ 1 = closure {1}

Tactic:
rw [closure_singleton_eq, one_eq_mrange]; congr 1; ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ (lTensor M (g ∘ₗ f)) x = (lTensor M g) ((lTensor M f) x)

Tactic:
by rw [lTensor_comp, coe_comp]; rfl

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

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure ↑M * closure ↑N

Tactic:
closure_eq,

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = M * closure ↑N
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
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
⊢ ∀ r ∈ ⊥, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _

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

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : IsScalarTower α A A
a : α
S T : Submodule R A
⊢ (a • span R ↑S) • T = a • span R ↑S • T

Tactic:
← T.span_eq,

Goal state after:
ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : IsScalarTower α A A
a : α
S T : Submodule R A
⊢ (a • span R ↑S) • span R ↑T = a • span R ↑S • span R ↑T
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : SMulCommClass α A A
a : α
S T : Submodule R A
⊢ a • span R ↑S • T = span R ↑S • a • T

Tactic:
← T.span_eq,

Goal state after:
ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : SMulCommClass α A A
a : α
S T : Submodule R A
⊢ a • span R ↑S • span R ↑T = span R ↑S • a • span R ↑T
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b - b * (a * b / b) ≺ b
⊢ False

Tactic:
sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b % b ≺ b
⊢ False
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' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (map f (I • comap f p)) ≤ I • comap f p

Tactic:
Submodule.comap_map_eq_of_injective hf

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ I • comap f p ≤ I • comap f p
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 ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
this : Fintype ι
⊢ ∑ i, Pi.single i 1 * r' i ∈ I

Tactic:
exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ ker (e.toRingHom.comp f) = ker f

Tactic:
by
  rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y = z ↔ x = y * z

Tactic:
obtain ⟨a, ha⟩ := h2

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
a : R
ha : x = y * a
⊢ x / y = z ↔ x = y * z
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
by
  rw [sup_comm] at h
  rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]

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

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

Tactic:
by
  obtain rfl | h := h.eq_or_lt
  · simp
  · 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.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Tactic:
by
  have : Ideal.span ({a} : Set α) ≠ ⊤ := by
    intro H
    rw [Ideal.span_singleton_eq_top] at H
    contradiction
  rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩
  use I, Imax
  apply H
  apply Ideal.subset_span
  exact Set.mem_singleton a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
by
  by_cases hg : gcd a b = 0
  · rw [gcd_eq_zero_iff] at hg
    rcases hg with ⟨rfl, rfl⟩
    exact
      (gcd_zero_left' (0 ^ k : α)).dvd.trans
        (pow_dvd_pow_of_dvd (gcd_zero_left' (0 : α)).symm.dvd _)
  · induction k with
    | zero => rw [pow_zero, pow_zero]; exact (gcd_one_right' a).dvd
    | succ k hk =>
      rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ LeftInverse (induced_map I ↑e.symm) (induced_map I ↑e)

Tactic:
rintro ⟨a⟩; exact congr_arg _ (e.left_inv ..)

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

Goal state before:
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬(a = 0 ∨ d = 0)
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
push Not at h_1

Goal state after:
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬(a = 0 ∨ d = 0)
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
push Not at h_1

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, toNat (Module.rank R (Fin n → R)) = 0

Tactic:
toNat_eq_zero

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i

Tactic:
by
  simp only [dotProduct, Finset.sum_apply, Finset.mul_sum]
  rw [Finset.sum_comm]

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

Goal state before:
pp: case inr.inl.hj
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ j ≠ g j'

Tactic:
exact g.symm_apply_eq.not.1 hj

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

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ single i j r (f (f.symm i)) (g j') = single (f.symm i) (g.symm j) r (f.symm i) j'

pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
⊢ single i j r (f (f.symm i)) (g (g.symm j)) = single (f.symm i) (g.symm j) r (f.symm i) (g.symm j)

Tactic:
· rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne]
    exact g.symm_apply_eq.not.1 hj

Goal state after:
case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
⊢ single i j r (f (f.symm i)) (g (g.symm j)) = single (f.symm i) (g.symm j) r (f.symm i) (g.symm j)
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
⊢ (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

Tactic:
by
  ext
  simp [mul_apply, map_sum]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
⊢ (finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)

Tactic:
ext
  rw [Submodule.mem_ideal_smul_span_iff_exists_sum]
  refine ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩
  rintro ⟨a, ha, rfl⟩
  classical
    refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
    rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
    · apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]
    · exact fun _ => zero_smul _ _

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

Goal state before:
pp: case pos
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : i = j
⊢ 0 ≤ 1 i j

Tactic:
subst hi

Goal state after:
case pos
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i : n
⊢ 0 ≤ 1 i i
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
i : ι
⊢ ∀ (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → motive f → motive (DFinsupp.single i b + f)

Tactic:
b

Goal state after:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
i : ι
b : β i
⊢ ∀ (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → motive f → motive (DFinsupp.single i b + f)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a : S
⊢ ∀ {b : S}, a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
b

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b : S
⊢ a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}