mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a', a ≤ a' ∧ b < u a'

Tactic:
obtain ⟨b', hb'⟩ := exists_gt b

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a', a ≤ a' ∧ b < u a'
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
by
  simp_rw [noZeroSMulDivisors_iff, or_iff_not_imp_left]
  exact ⟨fun h r hr m eq ↦ h eq hr, fun h r m eq hr ↦ h r hr m eq⟩

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N

Tactic:
· rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
⊢ False

Tactic:
obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ False
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker

Tactic:
refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
⊢ ⨆ m, (f ^ m).ker = (f ^ m).ker
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α = 0 ↔ IsEmpty α

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ by simp [cof]⟩

Goal state after:
α : Type u
inst✝ : Preorder α
x✝ : cof α = 0
⊢ IsEmpty α
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
rw [← neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case succ.inr
α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
hab : a < succ b
h : a < b
⊢ f a < f (succ b)

Tactic:
exact (IH h).trans (hs b)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : c.ord.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
← e,

Goal state after:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : (Ordinal.liftPrincipalSeg.toRelEmbedding o).card = c
⊢ ∃ c', c = lift.{u + 1, u} c'
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case pos
s : Set Ordinal.{u_3}
hs : BddAbove s
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
have hs' := bddAbove_add_one_image_iff.2 hs
    rw [csSup_le_iff' hs]
    exact fun x hx ↦ (lt_add_one _).le.trans (le_csSup hs' (mem_image_of_mem _ hx))

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < iSup f

Tactic:
rw [h]
    apply lt_lsub

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n < b ^ 1 ↔ n < b ∨ b ≤ 1

Tactic:
Nat.pow_one,

Goal state after:
case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n < b ↔ n < b ∨ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1

Tactic:
simpa using card_eq_nat (n := 1)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = (a * b + 0) / (a * c)

Tactic:
rw [add_zero]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ (o'.bsup fun a ha ↦ f (g a ha) ⋯) = o.bsup f

Tactic:
apply le_antisymm <;> refine bsup_le fun i hi => ?_
  · apply le_bsup
  · rw [← hg, lt_blsub_iff] at hi
    rcases hi with ⟨j, hj, hj'⟩
    exact (hf _ _ hj').trans (le_bsup _ _ _)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * d - a * b

Tactic:
← e,

Goal state after:
a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * b + c - a * b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1

Tactic:
rw [ne_eq, ← log_lt_log_succ_iff hb hn, not_lt]
  simp only [le_antisymm_iff, and_iff_right_iff_imp]
  exact fun _ ↦ log_monotone (le_add_right n 1)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = (x * y + 0) % (x * z)

Tactic:
rw [add_zero]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z) + 0

Tactic:
rw [add_zero]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, deriv f o = a

Tactic:
unfold deriv

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x ↦ f) o = a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o.card ≤ ℵ₀

Tactic:
· rwa [card_le_iff, succ_aleph0, ord_aleph]

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

Goal state before:
pp: case neg
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ Cardinal.lift.{u, v} c

Tactic:
apply (lift_card_iSup_le_sum_card ..).trans ((sum_le_lift_mk_mul_iSup_lift _).trans _)

Goal state after:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
i' : Ordinal.{u}
hi' : i' < type r'
hfg : f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'
⊢ f i < (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
exact hfg.trans_lt (lt_blsub _ _ _)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ ↑(f i) + 1 < (succ c).ord

Tactic:
exact (isSuccLimit_ord hc₀).add_one_lt (f i).2

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ range Subtype.val

Tactic:
Subtype.range_coe

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

Goal state before:
pp: case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ range Subtype.val

Tactic:
Subtype.range_coe

Goal state after:
case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
⊢ comapDomain h hh (single (h k) x) = single k x

Tactic:
by
  ext i
  rw [comapDomain_apply]
  obtain rfl | hik := Decidable.eq_or_ne i k
  · rw [single_eq_same, single_eq_same]
  · rw [single_eq_of_ne hik, single_eq_of_ne (hh.ne hik)]

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

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

Tactic:
rw [extendWith_none, single_eq_same]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i ↦ (fun x ↦ (e i) x) ∘ fun x ↦ (e i).symm x) ?h x = x

Tactic:
AddEquiv.self_comp_symm

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i ↦ id) ⋯ x = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ ∀ (i : ι), ((fun x ↦ (e i) x) ∘ fun x ↦ (e i).symm x) 0 = 0

Tactic:
AddEquiv.self_comp_symm

Goal state after:
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ ∀ (i : ι), id 0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0

Tactic:
specialize h {i, j} (Pi.single i c + Pi.single j d)

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
c d : R
h :
  ↑{i, j} ⊆ {i, j} →
    (∀ i_1 ∉ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0) →
      ∑ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 • f i_1 = 0 →
        ∀ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

Tactic:
rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ x ∈ {i, j}, x ∉ t → g x • f x = 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)
hsp : map f ⊤ = ⊤
⊢ Surjective ⇑f

Tactic:
Submodule.map_top

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)
hsp : f.range = ⊤
⊢ Surjective ⇑f
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ - χ) a = ψ a / χ a

Tactic:
sub_apply,

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ ψ a * χ (-a) = ψ a / χ a
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ ψ y = 1 y

Tactic:
rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ ψ (u * (↑hu.unit⁻¹ * y)) = 1 (u * (↑hu.unit⁻¹ * y))
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
List.ofFn_succ,

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ (s 0 :: List.ofFn fun i ↦ s i.succ).prod ↔ ∃ f, (↑(f 0) :: List.ofFn fun i ↦ ↑(f i.succ)).prod = a
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, ∀ x ∈ s, f x b ∈ u

Tactic:
@forall₂_comm α

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✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ (insert b₁ u).card = (s' ∪ insert b₁ t).card

Tactic:
by
            simp [Eq, hb₁t, hb₁s', hb₁u]

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

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

Tactic:
change ↑(npowRec n s) = (s : Set α) ^ n

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ {a ∈ A | f a = aH}

Tactic:
rw [mem_filter]

Goal state after:
case refine_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ A ∧ f a = aH
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ {b ∈ B | f b = bH}

Tactic:
rw [mem_filter]

Goal state after:
case refine_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ B ∧ f b = bH
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid α
n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ Set.univ ^ n = Set.univ

Tactic:
Set.univ_pow hn

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid α
n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ Set.univ = Set.univ
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
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Tactic:
have :=
    CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
      (Submodule.singleton_span_isCompactElement m) p

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : R ∙ m ≤ ⨆ i, p i → ∃ s, R ∙ m ≤ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : K[ℕ]
⊢ (x✝ • { toFinsupp := toFinsupp✝¹ }) • { toFinsupp := toFinsupp✝ } =
    x✝ • { toFinsupp := toFinsupp✝¹ } • { toFinsupp := toFinsupp✝ }

Tactic:
simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]

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
⊢ Submodule.map (↑e) p ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule

Tactic:
have : e.symm.toLinearMap ∘ₗ ((e ∘ₗ f) ∘ₗ e.symm.toLinearMap) ∘ₗ e = f := by ext; simp

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 ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝³ : Semiring R
inst✝² : (i : η) → AddCommMonoid (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ LinearIndependent R fun ji ↦ single ji.fst (v ji.fst ji.snd)

Tactic:
convert! (DFinsupp.linearIndependent_single _ hs).map_injOn _ DFinsupp.injective_pi_lapply.injOn

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case pos
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j, i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j, i'⟩

Tactic:
simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]

Goal state after:
case pos
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ({ toFun := fun f i ↦ (s i).repr (f i), map_add' := ⋯, map_smul' := ⋯ } (single j ((s j) i)) j) i' =
    (Finsupp.single ⟨j, i⟩ 1) ⟨j, i'⟩