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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_sdiff_of_notMem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa

Goal state after:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h✝ : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ f (f r) = f r

Tactic:
by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]

Goal state after:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
intro eq
    by_cases h : a₁ = a₂
    · refine Or.inl ⟨h, ?_⟩
      rwa [h, (single_injective a₂).eq_iff] at eq
    · rw [DFunLike.ext_iff] at eq
      have h₁ := eq a₁
      have h₂ := eq a₂
      grind

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ f a = 0 a

Tactic:
have : f.optionElim y (Option.some a) = (0 : Option α →₀ M) (Option.some a) := by
    rw [c]

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
this : (optionElim y f) (Option.some a) = 0 (Option.some a)
⊢ f a = 0 a
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
simp_rw [indicator]

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ s.card ≤ s.prod

Tactic:
rw [← Multiset.prod_replicate, ← Multiset.map_const]

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ (map (Function.const α a) s).prod ≤ s.prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (f a) b

Tactic:
by
  classical
    ext x
    simp only [single_apply, ← Equiv.eq_symm_apply, equivMapDomain_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = 0

Tactic:
refine Finset.sum_eq_zero fun i hi => if_neg ?_

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
⊢ ¬f i = f a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = 0

Tactic:
refine Finset.sum_eq_zero fun i hi => if_neg ?_

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
i : α
hi : i ∈ x.support
⊢ ¬f i = f a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg.h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ a ∉ Set.range ⇑f

Tactic:
assumption

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
exact ⟨fun x hx => hif hx rfl hx, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (filter (fun x ↦ a = x) f) a✝ = (single a (f a)) a✝

Tactic:
rw [filter_apply, single_apply]

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Codisjoint s t
⊢ Codisjoint (supported M R s) (supported M R t)

Tactic:
by
  rw [codisjoint_iff, eq_top_iff, ← supported_union,
    show s ∪ t = .univ from codisjoint_iff.mp h, supported_univ]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
⊢ range (natAdd m) = Ioi (castAdd n ⊤)

Tactic:
ext ⟨_, _⟩
  simp [range_natAdd, lt_def, ← Nat.succ_le_iff, Nat.one_le_iff_ne_zero.mpr (NeZero.ne m)]

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
⊢ b₁.repr = b₂.repr

Tactic:
by ext; apply h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : ¬HasFiniteMulSupport fun x ↦ 0
⊢ 1 ≤ ∏ᶠ (x : α), 1

Tactic:
exact finprod_one.symm.le

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
⊢ x ∈ span R (v '' s) ↔ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩
  · obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h
    refine ⟨l.support, hl, l ∘ (↑), ?_⟩
    rw [← hx]
    exact l.support.sum_coe_sort fun a ↦ l a • v a
  · rw [← hx]
    exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) ⋯.choose = ↑x

Tactic:
exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a - b = a.rev.rev - b

Tactic:
rev_rev

Goal state after:
n : ℕ
a b : Fin n
⊢ a - b = a - b
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.rev < b.rev.rev ↔ a.rev < b

Tactic:
rev_rev

Goal state after:
n : ℕ
a b : Fin n
⊢ a.rev < b ↔ a.rev < b
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
have : (i : ℕ) < n := Fin.val_lt_last h

Goal state after:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
c : R
x : M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0

Tactic:
have := b.isTorsionFree; exact smul_eq_zero

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

Goal state before:
pp: case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False

Tactic:
rw [y_0, epow_zero] at h; contradiction

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

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
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
by
  classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
  constructor
  · rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
  · rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) i

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
by
  simpa only [add_comm c, add_comm d] using h.add_iff_left

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

Goal state before:
pp: case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).sum fun i a ↦ a • v i) =
    (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).sum fun i a ↦ a • v i

Tactic:
Finsupp.embDomain_eq_mapDomain

Goal state after:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ((Finsupp.mapDomain (⇑(Embedding.subtype fun x ↦ x ∈ s)) l₁).sum fun i a ↦ a • v i) =
    (Finsupp.mapDomain (⇑(Embedding.subtype fun x ↦ x ∈ s)) l₂).sum fun i a ↦ a • v i
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
p a b : G
z : ℤ
inst✝ : IsAddTorsionFree G
hn : z ≠ 0
⊢ z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p]

Tactic:
by
  simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm, zsmul_right_inj hn]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ¬LinearIndepOn R v s ↔
    ∃ f g,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g

Tactic:
simp [linearIndepOn_iffₛ]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc < j

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inr
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

Tactic:
· rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
      castSucc_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
    · exact le_iff_val_le_val.2 (le_of_lt h)
    · rw [le_iff_val_le_val, val_succ]
      exact Nat.succ_le_of_lt h

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

Goal state before:
pp: case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ (a % c + b % c) % c + c = a % c + b % c

Tactic:
have h2 : (a % c + b % c) / c < 2 :=
        Nat.div_lt_of_lt_mul
          (by
            rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
      have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
      rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]

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

Goal state before:
pp: case insert
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
h4 : g a = 0
⊢ ∀ i ∈ insert a s, g i = 0

Tactic:
exact (Finset.forall_mem_insert ..).2 ⟨h4, h3⟩

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ Subsingleton ι

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} (Module.rank R N)
h' : Module.rank R N < ℵ₀
⊢ finrank R M ≤ finrank R N

Tactic:
simpa only [toNat_lift] using! toNat_le_toNat h (lift_lt_aleph0.mpr h')

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔ ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0

Tactic:
by
  classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, ofPred_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : x = a
⊢ b ∈ t

Tactic:
assumption

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ t₂
le1 : ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 : ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ⊆ ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
⊢ a ∈ t₁

Tactic:
obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩

Goal state after:
α : Type u_1
inst✝ : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
x✝ : (fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂ ≤ (fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁
a : α
ha : a ∈ t₂
le1 : ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).1 ≤ ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).1
le2 : ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₂).2 ⊆ ((fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)) t₁).2
a' : α
h' : a' ∈ ↑t₁
eq : ↑a' = ↑a
⊢ a ∈ t₁
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑(Quotient.out L • ↑s)

Tactic:
rw [← eq_class_eq_leftCoset]
        change
          (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃
            _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
        simp
        rfl

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
⊢ f'' a ha ∈ t.toFinset

Tactic:
by { rw [mem_toFinset] at ha ⊢; exact hf a ha }

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: case left
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite ↥?m.11

Tactic:
assumption

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: case right
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite (G ⧸ H)

Tactic:
assumption

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s)) a b → (leftRel (H.subgroupOf t)) ((inclusion h) a) ((inclusion h) b)

Tactic:
simp_rw [leftRel_eq]

Goal state after:
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ a⁻¹ * b ∈ H.subgroupOf s → ((inclusion h) a)⁻¹ * (inclusion h) b ∈ H.subgroupOf t
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ (leftRel (s.subgroupOf H)) a b → (leftRel (t.subgroupOf H)) (id a) (id b)

Tactic:
simp_rw [leftRel_eq]

Goal state after:
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ a⁻¹ * b ∈ s.subgroupOf H → (id a)⁻¹ * id b ∈ t.subgroupOf H
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ (leftRel s) a b → (leftRel t) (id a) (id b)

Tactic:
simp_rw [leftRel_eq]

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ a⁻¹ * b ∈ s → (id a)⁻¹ * id b ∈ t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
this : Infinite ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ ⇑(sInf (Set.range f)) = ⨅ i, ⇑(f i)

Tactic:
coe_sInf,

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ sInf (DFunLike.coe '' Set.range f) = ⨅ i, ⇑(f i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hI : I.Finite
hIJ : Codisjoint I J
⊢ ⨅ i ∈ J, (proj i).ker ≤ ⨆ i ∈ I, (single R φ i).range

Tactic:
lift I to Finset ι using hI

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
⊢ ⨅ i ∈ J, (proj i).ker ≤ ⨆ i ∈ ↑I, (single R φ i).range
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ f x = ∑ i, x i • f fun j ↦ if i = j then 1 else 0

Tactic:
by
  conv_lhs => rw [pi_eq_sum_univ x, map_sum]
  refine Finset.sum_congr rfl (fun _ _ => ?_)
  rw [map_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ (single R φ i) x j ∈ p j

Tactic:
rcases eq_or_ne j i with rfl | hne <;> simp [*]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
⊢ ∀ (a : M₂) (b : M₃) (x : M), f x = a → ∀ (x : M), g x = b → ∃ y, (f y, g y) = (a, b)

Tactic:
rintro _ _ x rfl y rfl

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
⊢ ∃ y_1, (f y_1, g y_1) = (f x, g y)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -max (-toZ i0 (pred^[n.succ] i0)) 0

Tactic:
toZ_of_lt this,

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ -↑(Nat.find ⋯) = -max (- -↑(Nat.find ⋯)) 0
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.1 ≤ n

Tactic:
rw [le_iff_exists_mul]
  use kl.2
  rwa [mem_mulAntidiagonal, eq_comm] at hlk

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ m ≤ k

Tactic:
exact hkm

Goal state after: