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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
· filter_upwards with i
    simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t

Tactic:
mem_iInf_of_directed h,

Goal state after:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.1 i.2 ∧ s i.1 i.2 ⊆ t

Tactic:
mem_iInf_of_directed h,

Goal state after:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ i, p i.1 i.2 ∧ s i.1 i.2 ⊆ t
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ ∃ i, ∃ (_ : i ∈ s), x ∈ Ici i

Tactic:
exact ⟨y, hys, hyx.le⟩

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (map Prod.mk f).seq g = (map (fun b a ↦ (a, b)) g).seq f

Tactic:
refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
  · rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
    grw [← hs]
    rw [← Set.prod_image_seq_comm]
    exact seq_mem_seq (image_mem_map ht) hu
  · rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
    grw [← hs]
    rw [Set.prod_image_seq_comm]
    exact seq_mem_seq (image_mem_map ht) hu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ 0 < a • b ↔ 0 < b

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
exact le_sup_left

Goal state after:
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]; simp only [neg_pos, neg_nonneg]

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : Module.Finite R M
⊢ Module.Finite A M

Tactic:
rw [finite_def, fg_def] at hM ⊢
  obtain ⟨S, hSfin, hSgen⟩ := hM
  refine ⟨S, hSfin, eq_top_iff.mpr ?_⟩
  have := span_le_restrictScalars R A S
  rwa [hSgen] at this

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
hd₃ : a ∈ s
b : α
hbd : b ∈ d
hb : Ici b ∩ d ⊆ s
⊢ (d ∩ s).Nonempty

Tactic:
exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ↑((enum s hs) a) ≤ ↑⟨o, ho⟩

Tactic:
Subtype.coe_le_coe,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ (enum s hs) a ≤ ⟨o, ho⟩
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ b, enumOrd s ↑b ∈ s

Tactic:
have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩

Goal state after:
case refine_1
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty ↑(Iio o)
⊢ ⨆ b, enumOrd s ↑b ∈ s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ IsLUB (f '' Iio a✝) (f a✝)

Tactic:
by
      rw [← h₂ _ ho]
      simpa [IsLUB, upperBounds, lowerBounds, IsLeast, bsup_le_iff] using le_bsup _

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ IsSuccLimit (a + b) ↔ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
by
  refine ⟨fun h ↦ ?_, by grind [isSuccLimit_add]⟩
  rcases eq_or_ne b 0 with (rfl | h')
  · grind
  rw [← add_sub_cancel a b]
  exact .inl <| isSuccLimit_sub h.isSuccPrelimit <| lt_add_of_pos_right a h'.pos

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

Goal state before:
pp: n : ℕ
x : Fin n
⊢ Fintype.card ↑(Iio x) = ↑x

Tactic:
exact Fintype.card_fin_lt_of_le x.is_le'

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

Goal state before:
pp: case case1.inr
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]

Goal state after:
case case1.inr.hb
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ x > b ^ y
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) ≤ ↑(n + 1)

Tactic:
apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)

Goal state after:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
⊢ preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c

Tactic:
obtain rfl | ho := eq_or_ne o 0

Goal state after:
case inl
c : Cardinal.{u_1}
l : IsSuccPrelimit 0
⊢ preAleph 0 ≤ c ↔ ∀ o' < 0, preAleph o' ≤ c

case inr
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
ho : o ≠ 0
⊢ preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ a * b < c

Tactic:
apply (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt

Goal state after:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ max a b * max a b < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rw [max_le_iff]
  refine ⟨fun h => ?_, ?_⟩
  · rcases le_or_gt ℵ₀ a with ha | ha
    · have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
      left
      rw [and_assoc]
      use ha
      constructor
      · rw [← not_lt]
        exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
      · rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm
    right
    by_cases h2a : a = 0
    · exact Or.inr h2a
    have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
    left
    rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
    · contradiction
    · contradiction
    rw [← Ne] at h2a
    rw [← Cardinal.one_le_iff_ne_zero] at h2a hb
    norm_cast at h2a hb h ⊢
    apply le_antisymm _ hb
    rw [← not_lt]
    apply fun h2b => ne_of_gt _ h
    conv_rhs => left; rw [← mul_one n]
    rw [Nat.mul_lt_mul_left]
    · exact id
    apply Nat.lt_of_succ_le h2a
  · rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
    · rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
    all_goals simp

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

Goal state before:
pp: case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
b : Ordinal.{u}
hb : b ∈ Iio (⨆ i, f i + 1)
⊢ ∃ y ∈ range fun i ↦ ⟨f i, ⋯⟩, ⟨b, hb⟩ ≤ y

Tactic:
rw [mem_Iio, Ordinal.lt_iSup_add_one_iff] at hb

Goal state after:
case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
b : Ordinal.{u}
hb✝ : b ∈ Iio (⨆ i, f i + 1)
hb : ∃ i, b ≤ f i
⊢ ∃ y ∈ range fun i ↦ ⟨f i, ⋯⟩, ⟨b, hb✝⟩ ≤ y
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = a.cof

Tactic:
simpa [← lift_cof] using lift_cof_iSup_add_one hf

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _) <;> apply card_le_card

Goal state after:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a ≤ a ^ b

a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} #(List ι) < c.cof

Tactic:
apply (Cardinal.lift_le.2 (mk_list_le_max _)).trans_lt

Goal state after:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} (max ℵ₀ #ι) < c.cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a ≤ a ^ b

pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b

Tactic:
· exact left_le_opow a (omega0_pos.trans_le hb)

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) o

Tactic:
obtain ⟨a, rfl⟩ := mem_range_omega_iff.2 ⟨ho, h⟩
  exact isPrincipal_opow_omega a

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) c.ord

Tactic:
by
  apply (isInitial_ord c).isPrincipal_opow
  rwa [omega0_le_ord]

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

Goal state before:
pp: case le_cof_ord
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
⊢ False

Tactic:
apply hf.iSup_add_one_eq.not_lt

Goal state after:
case le_cof_ord
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, ↑(f i) + 1 < (succ c).ord
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
⊢ ∃ a, Infinite ↑(f ⁻¹' {a})

Tactic:
Cardinal.infinite_iff

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})
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
v' : Option κ → M := fun o ↦ o.elim (b i) v
k : κ
⊢ v k ∈ range v'

Tactic:
exact ⟨some k, rfl⟩

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (preBeth ∘ ord) c ≤ c

Tactic:
apply (isNormal_preBeth.le_iff_forall_le (isSuccLimit_ord hc.aleph0_lt.le)).2

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ∀ a' < c.ord, preBeth a' ≤ c
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ v.prod f = ∏ i, f i (equivFunOnFintype v i)

Tactic:
suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∏ i ∈ v.support, f i (v i) = ∏ i, f i (v i)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = (RingHom.id R) c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
i : ι
x : N
h : x ∈ p i
⊢ (ind.linearEquiv iSup_top).symm x = single i ⟨x, h⟩

Tactic:
simp [← LinearEquiv.eq_symm_apply, iSupIndep.linearEquiv]

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, x + y] ↔ LinearIndependent R ![x, y]

Tactic:
suffices ∀ x y : M, LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y] from
    ⟨this x y, fun h ↦ by simpa using this (-x) (x + y) (by simpa)⟩
  simp only [LinearIndependent.pair_iff]
  intro x y h s t h'
  obtain ⟨h₁, h₂⟩ := h (s - t) t (by rw [sub_smul, smul_add, ← h']; abel)
  rw [h₂, sub_zero] at h₁
  tauto

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ⁻¹ = ψ.mulShift (-1)

Tactic:
by
  ext
  rw [inv_apply, mulShift_apply, neg_mul, one_mul]

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
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z

Tactic:
have a0 : a ≠ 0 := by
    rintro rfl
    simp_all

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective fun a ↦ f a b
⊢ #(image₂ f s {b}) = #s

Tactic:
rw [image₂_singleton_right, card_image_of_injective _ hf]

Goal state after:
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 β
⊢ ↑(image₂ f s t) = ↑(image₂ (fun a b ↦ f b a) t s)

Tactic:
push_cast
    exact image2_swap _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < k

Tactic:
exact i.2

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ ↑s / ↑t ↔ ¬Disjoint ↑s ↑t

Tactic:
Set.one_mem_div_iff

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ ¬Disjoint ↑s ↑t ↔ ¬Disjoint ↑s ↑t
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
have hcard : 1 < #C ∨ 1 < #D := by simp_rw [C, D, card_map]; exact hc.2.2

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
⊢ ∃ 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.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✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
⊢ (Pi.basis s).repr (single j ((s j) i)) = Finsupp.single ⟨j, i⟩ 1

Tactic:
ext ⟨j', i'⟩

Goal state after:
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 : ιs j
j' : η
i' : ιs j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case neg
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 : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ({ toFun := fun f i ↦ (s i).repr (f i), map_add' := ⋯, map_smul' := ⋯, invFun := fun f i ↦ (s i).repr.symm (f i),
          left_inv := ⋯, right_inv := ⋯ }
        (single j ((s j) i)) j')
      i' =
    (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
dsimp

Goal state after:
case neg
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 : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ((s j').repr (single j ((s j) i) j')) i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
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:
rw [Set.Finite, ← Module.finite_iff_finite (R := R)]

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
⊢ Module.Finite R ↑↑(span R ↑s)
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
⊢ Module.Finite R ↑↑(span R ↑s)

Tactic:
dsimp

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
⊢ Module.Finite R ↥(span R ↑s)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
i : ι
h : i ∉ s.sup fun m ↦ (x m).support
⊢ lapply i ∘ₗ x = 0

Tactic:
exact LinearMap.ext_on span_s (by simpa using! h)

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
hst : s ×ˢ t ⊆ SetRel.id
⊢ ∃ x, s = {x} ∧ t = {x}

Tactic:
obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := ht
  simp only [Set.prod_subset_iff, mem_id] at hst
  obtain rfl := hst _ ha _ hb
  simp only [Set.eq_singleton_iff_unique_mem, and_assoc]
  exact ⟨a, ha, (hst · · _ hb), hb, (hst _ ha · · |>.symm)⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
x✝ : Fin (((fun x ↦ fromListIsChain ↑x ⋯ ⋯) ((fun x ↦ ⟨x.toList, ⋯⟩) x)).length + 1)
⊢ ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) ((fun x ↦ ⟨x.toList, ⋯⟩) x)).toFun x✝ = (x.toFun ∘ Fin.cast ⋯) x✝

Tactic:
dsimp

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
x✝ : Fin (((fun x ↦ fromListIsChain ↑x ⋯ ⋯) ((fun x ↦ ⟨x.toList, ⋯⟩) x)).length + 1)
⊢ (fromListIsChain x.toList ⋯ ⋯).toFun x✝ = x.toFun (Fin.cast ⋯ x✝)