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

Goal state before:
pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
classical
  let := linearOrderOfSTO r
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof

Tactic:
obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ #α < #α ^ (#α).ord.cof
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
⊢ False

Tactic:
let v' (o : Option κ) : M := o.elim (b i) v

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'
α : Type u
s : Set α
c : Cardinal.{u}
⊢ Injective fun t ↦ Subtype.val ⁻¹' ↑t

Tactic:
rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h

Goal state after:
case inj'
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t ↦ Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t ↦ Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ⟨t, ⋯⟩ = ⟨t', ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{u, v} #↑(range ⇑f)

Tactic:
rw [mk_range_eq_of_injective]

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Injective ⇑f
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]

Goal state after:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
rcases eq_or_ne j i with (rfl | h)

Goal state after:
case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
j : ι
⊢ (erase j f) j = (f - single j (f j)) j

case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧).eval = fun x ↦ ⟦a x⟧

Tactic:
finChoice_eq

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x ↦ ⟦a x⟧
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ (finChoice fun x ↦ ⟦a x⟧).liftOn f h = f a

Tactic:
finChoice_eq

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ ⟦a⟧.liftOn f h = f a
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧).eval = fun x ↦ ⟦a x⟧

Tactic:
finChoice_eq

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x ↦ ⟦a x⟧
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ Quotient.hrecOn (finChoice fun x ↦ ⟦a x⟧) f h ≍ f a

Tactic:
finChoice_eq

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ Quotient.hrecOn ⟦a⟧ f h ≍ f a
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
h : ¬i = i'
⊢ (mapRange f hf (single i b)) i' = (single i (f i b)) i'

Tactic:
simp [h, hf]

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

Goal state before:
pp: ι : 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)

Tactic:
enter [

Goal state after:
ι : 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)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (span R (v '' s)) (span R (v '' t))

Tactic:
rw [Finsupp.span_image_eq_map_linearCombination, Finsupp.span_image_eq_map_linearCombination]
  refine Submodule.codisjoint_map ?_ (Finsupp.codisjoint_supported_supported hst)
  rwa [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

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
⊢ (∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ s = 0 ∧ t = 0
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
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ (∀ (s t : R), s • u • x + t • v • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • u • x + t • v • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0
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
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
⊢ (∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

case refine_2
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
specialize h (u • s) (u • t) (by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst])

Goal state after:
case refine_2
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
s t : R
h : u • s = 0 ∧ u • t = 0
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0
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
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
c : ι →₀ R
this : (c.sum fun i a ↦ a • v i) ∈ span R (Set.range v)
hx : (c.sum fun a b ↦ b • f (v a)) = 0
⊢ (c.sum fun i a ↦ a • v i) = 0

Tactic:
obtain rfl := linearIndependent_iff.mp hli c hx

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
this : (Finsupp.sum 0 fun i a ↦ a • v i) ∈ span R (Set.range v)
hx : (Finsupp.sum 0 fun a b ↦ b • f (v a)) = 0
⊢ (Finsupp.sum 0 fun i a ↦ a • v i) = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∑ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

Tactic:
coe_sum,

Goal state after:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∏ i ∈ s, ⇑(ψ i)) a = ∏ i ∈ s, (ψ i) a
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Nontrivial R
m : M
s : Set M
⊢ single m 1 ∈ Submodule.span R ((fun x ↦ single x 1) '' s) ↔ m ∈ s

Tactic:
refine (Set.mem_image_equiv (f := (coeffLinearEquiv R).toEquiv)).symm.trans ?_
  change _ ∈ (Submodule.span R _).map (coeffLinearEquiv R).toLinearMap ↔ _
  simp [Submodule.map_span, ← Set.image_comp, Finsupp.single_mem_span_single]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ (fun a b ↦ f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
exact image_image₂_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (↑s ∩ ↑t) (↑s ∪ ↑t) ⊆ image2 f ↑s ↑t

Tactic:
exact image2_inter_union_subset hf

Goal state after:
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
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ s ⊆ ↑(span K ↑({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}))

Tactic:
by rwa [eq]

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
a✝ : M × M
⊢ a✝ ∈ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} ↔
    a✝ ∈ {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}

Tactic:
simp only [mem_filter, mem_product, hs, and_comm]

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
· rw [hp hps h1, mul_zero]

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
rcases not_and_or.mp hnotMem with af | bg

Goal state after:
case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
af : a0 ∉ f.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * (x + y) = ↑a * x + ↑a * y

Tactic:
mul_add

Goal state after:
R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ ↑a * x + ↑a * y = ↑a * x + ↑a * y
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * (x + y) = ↑a * x + ↑a * y

Tactic:
mul_add

Goal state after:
R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ ↑a * x + ↑a * y = ↑a * x + ↑a * y
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
⊢ 0 < #s

Tactic:
rwa [length_sort] at h

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_1.single
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ s • single (u i) 1 ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ ⨆ a ∈ S, a ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
iSup_subtype',

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ ⨆ x, ↑x ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
Module: Mathlib.Order.Sublattice

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
f : ι → Sublattice α
⊢ ↑(⨅ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp [iInf]

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
m✝ : S
toFinsupp✝ : R[ℕ]
⊢ MulOpposite.op m✝ • { toFinsupp := toFinsupp✝ } = m✝ • { toFinsupp := toFinsupp✝ }

Tactic:
simp_rw [← ofFinsupp_smul, op_smul_eq_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ (↑(span R ↑s)).Finite

Tactic:
Set.Finite,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Finite ↑↑(span R ↑s)
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 : ι), TwoUniqueProds (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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA : A.Nonempty
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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
obtain ⟨p1, h1, p2, h2, hne, hi1, hi2⟩ := uniqueMul_of_one_lt_card (Nat.one_lt_mul_iff.mpr
      ⟨card_pos.2 (hA.image _), card_pos.2 (hB.image _), hc.imp And.left And.left⟩)

Goal state after:
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 : ι), TwoUniqueProds (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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA : A.Nonempty
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
p1 : G i × G i
h1 : p1 ∈ image (fun x ↦ x i) A ×ˢ image (fun x ↦ x i) B
p2 : G i × G i
h2 : p2 ∈ image (fun x ↦ x i) A ×ˢ image (fun x ↦ x i) B
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case right
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.subtype.coprod q.subtype).range = ⊤

Tactic:
← sup_eq_range,

Goal state after:
case right
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 ⊔ q = ⊤
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (⊤ ⊓ g.ker).FG

Tactic:
top_inf_eq

Goal state after:
case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ g.ker.FG
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:
simpa only [map_one, comm₂₃] using hx₂

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]; exact le_iInf₂ h

Goal state after: