mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
← @blsub_eq_lsub' ι r hr

Goal state after:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ lift.{u, u} #α ≠ lift.{u, u} #β ↔ #α ≠ #β

Tactic:
lift_id,

Goal state after:
α β : Type u
⊢ #α ≠ lift.{u, u} #β ↔ #α ≠ #β
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #↑s < c
⊢ (∀ (i : ↑s), #↑(t ↑i ⋯) < c) ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c

Tactic:
SetCoe.forall'

Goal state after:
c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #↑s < c
⊢ (∀ (i : ↑s), #↑(t ↑i ⋯) < c) ↔ ∀ (x : ↑s), #↑(t ↑x ⋯) < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
dif_neg h'

Goal state after:
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr { down := 0 } = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ g.toFun (Classical.choose this) = g.toFun ⟨x, h⟩

Tactic:
exact Classical.choose_spec this

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
support_update_ne_zero f _ hb

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ insert i f.support ↔ j ∈ insert i f.support
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ 0 (h i✝) = 0

Tactic:
zero_apply

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ 0 (h i✝) = 0

Tactic:
zero_apply

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ 0 j = 0

Tactic:
zero_apply

Goal state after:
case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case e'_2
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
⊢ (sumZeroHom fun i_1 ↦ ↑(Pi.single i φ i_1)) = sumZeroHom (Pi.single i ↑φ)

Tactic:
conv_lhs =>
      enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ (∀ (x : M₁), x✝ (f x) = 0 x) ↔ ∀ (i : M₁), x✝ (f i) = 0

Tactic:
zero_apply

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]

Tactic:
by
  rw [pair_symm_iff, pair_neg_left_iff, pair_symm_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')

Tactic:
rw [ker_comp, ker_mkQ]

Goal state after:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
v : Fin (n + 1) → V
⊢ LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ span K (range (Fin.tail v))

Tactic:
by
  rw [← linearIndependent_finCons, Fin.cons_self_tail]

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g ↑s ↑t) ↑u = image2 g' (image2 f' ↑s ↑u) ↑t

Tactic:
exact image2_right_comm h_right_comm

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m₁ m₂ m₁' m₂' : M
hr₁ : r₁ ≠ 0
hr₂ : r₂ ≠ 0
⊢ single m₁ r₁ + single m₂ r₂ = single m₁' r₁ + single m₂' r₂ ↔
    m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = m₂'

Tactic:
simp [← coeff_inj, single_add_single_eq_single_add_single, *]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ map opEquiv.toEmbedding (s ^ n * s) = map opEquiv.toEmbedding s * map opEquiv.toEmbedding s ^ n

Tactic:
map_op_mul,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ map opEquiv.toEmbedding s * map opEquiv.toEmbedding (s ^ n) =
    map opEquiv.toEmbedding s * map opEquiv.toEmbedding s ^ n
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := toFinsupp✝ }.support = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0

Tactic:
simp [support]

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

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

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.toFinsupp.coeff.sum fun m₁ r₁ ↦ q.toFinsupp.coeff.sum fun m₂ r₂ ↦ single (m₁ + m₂) (r₁ * r₂)) =
    ∑ x ∈ p.toFinsupp.coeff.support,
      ∑ x_1 ∈ q.toFinsupp.coeff.support, single (x + x_1) (p.toFinsupp.coeff x * q.toFinsupp.coeff x_1)

Tactic:
Finsupp.sum

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).support = p.support.erase n

Tactic:
simp [support]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ Submodule.map (↑e) p ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule

Tactic:
LinearEquiv.conj_apply,

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ Submodule.map (↑e) p ∈ invtSubmodule ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ↔ p ∈ f.invtSubmodule
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support = p.support

Tactic:
simp [support]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Semiring R
inst✝ : DecidableEq ι
⊢ LinearIndependent R ((fun i ↦ single i 1) ∘ ⇑(Equiv.sigmaPUnit ι))

Tactic:
exact Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R))
    <| by simp +contextual [Fintype.linearIndependent_iffₛ]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s

Tactic:
have h1 := map_one φ
  classical
  have := Fintype.ofFinite G
  simp only [← Finset.univ_sum_single (1 : G → k), Pi.one_apply, map_sum] at h1
  obtain ⟨s, hs⟩ : ∃ (s : G), φ (Pi.single s 1) ≠ 0 := by
    by_contra
    simp_all
  have h2 : ∀ t ≠ s, φ (Pi.single t 1) = 0 := by
    refine fun _ _ ↦ (eq_zero_or_eq_zero_of_mul_eq_zero ?_).resolve_left hs
    rw [← map_mul]
    convert! map_zero φ
    ext u
    by_cases u = s <;> simp_all
  have h3 : φ (Pi.single s 1) = 1 := by
    rwa [Fintype.sum_eq_single s h2] at h1
  use s
  refine AlgHom.toLinearMap_injective ((Pi.basisFun k G).ext fun t ↦ ?_)
  by_cases t = s <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
⊢ (p.projection q hpq).ker = q

Tactic:
simp [projection, ker_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ (p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p ⋯) ⋯ = LinearMap.id

Tactic:
by ext; simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x✝ : ↥p
x : E
hx : x ∈ p
⊢ ↑((codRestrict p ↑f ⋯) ↑⟨x, hx⟩) = ↑⟨x, hx⟩

Tactic:
obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
      exact DFunLike.congr_fun f.2.1 x

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a - ⨅ i, f i = ⨆ i, a - f i

Tactic:
by
  refine eq_of_forall_ge_iff fun c => ?_
  rw [tsub_le_iff_right, add_comm, iInf_add]
  simp [tsub_le_iff_right, add_comm]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ coheight a = ⨆ p, ⨆ (_ : a ≤ RelSeries.head p), ↑p.length

Tactic:
by
  apply Equiv.iSup_congr ⟨RelSeries.reverse, RelSeries.reverse, fun _ ↦ RelSeries.reverse_reverse _,
    fun _ ↦ RelSeries.reverse_reverse _⟩
  congr! 1

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ (p.eraseLast.last, p.last) ∈ r

Tactic:
simp only [last, Fin.last, eraseLast_length, eraseLast_toFun]

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ (p.toFun ⟨p.length - 1, ⋯⟩, p.toFun ⟨p.length, ⋯⟩) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp.zero
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∃ x, x.length = 0

Tactic:
refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑(height a) ≤ krullDim α

Tactic:
have : Nonempty α := ⟨a⟩
  rw [krullDim_eq_iSup_length]
  simp only [WithBot.coe_le_coe]
  exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : P →ₗ[R] M ⊗[R] N
⊢ (↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N)) ∘ₗ f = f

Tactic:
comm_comp_comm,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : P →ₗ[R] M ⊗[R] N
⊢ LinearMap.id ∘ₗ f = f
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ -0 + 0 = 0

Tactic:
by rw [add_zero]; apply (Neg.aux R).map_zero

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * y * z

Tactic:
mul_assoc b

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_1
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μ :
  (if Exists.choose h ∈ t then μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x else 0) +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
⊢ ∑ i ∈ t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) i * ∏ j ∈ t \ {i}, s j = 1

pp: R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : 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
⊢ Decidable (Exists.choose h ∈ t)

Tactic:
← sum_pi_single',

Goal state after:
case cons.mp.refine_1
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μ :
  ∑ a' ∈ t, Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) a' +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
⊢ ∑ i ∈ t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) i * ∏ j ∈ t \ {i}, s j = 1
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
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → (x + y) • s ∈ ⨆ i, t✝ i • N

Tactic:
simp_rw [add_smul]

Goal state after:
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
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → x • s + y • s ∈ ⨆ i, t✝ i • 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
inst✝ : IsScalarTower R A A
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊥ ^ (n + 2) = ⊥

Tactic:
rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]

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

Goal state before:
pp: case succ.succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n + 1 ≠ 0 → (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid

Tactic:
ih n.succ_ne_zero

Goal state after:
case succ.succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n + 1 ≠ 0 → (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
⊢ M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid
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 : Submodule R A
| M * 1

Tactic:
rw [one_eq_span, ← span_eq M]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
| span R ↑M * (R ∙ 1)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N * map (↑(opLinearEquiv R).symm) M)

Tactic:
map_op_mul,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) M) *
      map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N)
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ᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(LinearEquiv.refl R Aᵐᵒᵖ)) (M * N) = map (↑(LinearEquiv.refl R Aᵐᵒᵖ)) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ)) N

Tactic:
LinearEquiv.refl_toLinearMap,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
rw [Finset.forall_mem_insert] at H

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : x ∈ Module.annihilator R M'
⊢ x ∈ Module.annihilator R M

Tactic:
by
  rw [Module.mem_annihilator] at h ⊢; exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
rw [h, zero_mul]
    rw [EuclideanDomain.gcd_eq_zero_iff] at h
    rw [h.1, zero_mul]

Goal state after:
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 : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N = ⊥

Tactic:
← le_bot_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N ≤ ⊥
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) = GCDMonoid.gcd (normalize a) (fold GCDMonoid.gcd 0 (s.erase a))
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
rw [gcd_union]

Goal state after:
α : 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) = {x ∈ s | f x ≠ 0}.gcd f
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
⊢ normUnit ↑u = u⁻¹

Tactic:
nontriviality α; convert normUnit_mul_units u one_ne_zero using 1 <;> simp

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

Goal state before:
pp: case right
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}

Tactic:
exact Set.mem_singleton a

Goal state after: