mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)

Tactic:
refine (Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_
  rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α →₀ β →₀ M
⊢ (↑f.support).PairwiseDisjoint fun a ↦ map (Embedding.sectR a β) (f a).support

Tactic:
intro a₁ _ a₂ _ hne

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α →₀ β →₀ M
a₁ : α
a✝¹ : a₁ ∈ ↑f.support
a₂ : α
a✝ : a₂ ∈ ↑f.support
hne : a₁ ≠ a₂
⊢ (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ a₂
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
rw [← Finset.card_filter_add_card_filter_not fun i ↦ f i = ∅, add_comm]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case neg
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x

Tactic:
· calc ∏ x ∈ S', f x
        ≤ ∏ x ∈ S.erase d ∪ {d'}, f x := Finset.prod_le_prod_of_subset' hS'
      _ = (∏ x ∈ S.erase d, f x) * f d' := by
          rw [Finset.prod_union (Finset.disjoint_singleton_right.mpr
            (fun h ↦ hd'S (Finset.mem_of_mem_erase h))), Finset.prod_singleton]
      _ < (∏ x ∈ S.erase d, f x) * f d := mul_lt_mul_right hlt _
      _ = ∏ x ∈ S, f x := Finset.prod_erase_mul S f hd_mem

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x

Tactic:
exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ l.splitSupport ↔ l.split i ≠ 0

Tactic:
classical rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]
  simp only [Finset.mem_preimage, exists_and_right, exists_eq_right, mem_support_iff,
    Sigma.exists, Ne]

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
f : α ↪ β
x : β →₀ M
⊢ x ∈ Set.range (embDomain f) ↔ ↑x.support ⊆ Set.range ⇑f

Tactic:
convert! mem_range_mapDomain_iff _ f.injective _
  · ext; rw [embDomain_eq_mapDomain]
  · grind

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ b.equivFun (b i) j = if i = j then 1 else 0

Tactic:
b.equivFun_apply,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (b.repr (b i)) j = if i = j then 1 else 0
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ (f.symm x * y) • z = x • y • z

Tactic:
mul_smul,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ f.symm x • y • z = x • y • z
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (∑ x, if x = i then r • v x else 0) = r • v i

Tactic:
Finset.sum_ite_eq',

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (if i ∈ Finset.univ then r • v i else 0) = r • v i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f g : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ ↑b.repr =
    linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr + linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ ↑b.repr

Tactic:
refine b.ext fun i => ?_
    simp

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
c : S
f : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ ↑b.repr =
    (RingHom.id S) c • linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr

Tactic:
refine b.ext fun i => ?_
    simp

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M →ₗ[R] M'
⊢ (fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) ((fun f i ↦ f (b i)) f) = f

Tactic:
refine b.ext fun i => ?_
    simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (fun a ↦ (a / ↑n, Fin.ofNat n (a.natMod ↑n))) ((fun p ↦ p.1 * ↑n + ↑↑p.2) (q, ⟨r, hrn⟩)) = (q, ⟨r, hrn⟩)

Tactic:
simp only [Prod.mk_inj, Fin.ext_iff]
    obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn
    rw [Int.add_comm, add_mul_ediv_right _ _ (natCast_eq_zero.not.2 (NeZero.ne n)),
      ediv_eq_zero_of_lt h1 h2, natMod, add_mul_emod_self_right, emod_eq_of_lt h1 h2, toNat_natCast]
    exact ⟨q.zero_add, Fin.val_cast_of_lt hrn⟩

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case succ
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1 + 1), ⋯⟩) = v (i + i + 1)

Tactic:
split_ifs with h <;> congr
    · simp [Nat.mod_eq_of_lt, h]
    · rw [Fin.val_mk, not_lt] at h
      simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]
      refine (Nat.mod_eq_of_lt ?_).symm
      lia

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a

Tactic:
rw [mul_finsum]

Goal state after:
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ ∑ᶠ (a : α), r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1

Tactic:
by
  cases n
  · simp
  split_ifs with h
  · simp [h]
  exact val_sub_one_of_ne_zero h

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
classical
  by_cases hr : r = 0
  · simp_all
  by_cases h : f.support.Finite
  · exact finsum_mul' f r h
  simp [finsum_def, HasFiniteSupport, h, (by aesop : (f · * r).support = f.support)]

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

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
have hf' : HasFiniteMulSupport fun i ↦ f i a := by fun_prop (disch := simp)

Goal state after:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)

Tactic:
finprod_mem_finset_eq_prod

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
⊢ ∏ i, f i = (List.map f (List.finRange n)).prod

Tactic:
by
  rw [← List.ofFn_eq_map, prod_ofFn]

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
H : ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i, (f ∘ Subtype.val) i • (v ∘ Subtype.val) i = ∑ i, (g ∘ Subtype.val) i • (v ∘ Subtype.val) i

Tactic:
by simpa only [← s.sum_coe_sort] using! eq

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
hv : LinearIndependent R v
i : ι
x : ↥(span R (range v))
hx : ↑x = v i
⊢ hv.repr x = Finsupp.single i 1

Tactic:
apply hv.repr_eq
  simp [Finsupp.linearCombination_single, hx]

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

Goal state before:
pp: n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

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

Goal state before:
pp: b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.gcd n ∣ 1

Tactic:
← Nat.modEq_zero_iff_dvd

Goal state after:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 1 ≡ 0 [MOD a.gcd n]
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
· have := hs.fintype
    simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
by
  classical
  obtain hs | hs := s.finite_or_infinite
  · have := hs.fintype
    simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
  · have := hs.to_subtype
    have := (hs.image hf).to_subtype
    simp [Nat.card_eq_zero_of_infinite]

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

Goal state before:
pp: α : Type u_3
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
rw [← le_one_iff_subsingleton]

Goal state after:
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ card (α → β) = card β ^ card α

Tactic:
· simp only [card_eq_top_of_infinite]
      rw [top_epow]
      rwa [card_ne_zero_iff_nonempty]

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

Goal state before:
pp: case refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
· refine ⟨.map ⟨_, v_ind.injective⟩ .univ, by simp, ?_⟩
    simpa using (linearIndepOn_id_range_iff v_ind.injective).mpr v_ind

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = ↑h.toFinset.card

Tactic:
toFinite_toFinset,

Goal state after:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = ↑s.toFinset.card
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ ?b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
apply Cardinal.lift_le.mpr

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ ?m.69 ≤ ⨆ ι, #↑↑ι

R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ Cardinal.{v}
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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

Tactic:
rintro hv f hf i hi
    rw [← s.sum_attach] at hf
    exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < s.ncard + t.ncard
⊢ (s ∩ t).Nonempty

Tactic:
rw [← ncard_union_add_ncard_inter s t] at h
  replace h := (s ∪ t).ncard_le_card.trans_lt h
  rwa [lt_add_iff_pos_right, ncard_pos] at h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ p.quotientRel x y ↔ -(x - y) ∈ p

Tactic:
rw [quotientRel, leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
      rfl

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

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : f a = w * y
fb : f b = x * z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
rw [← f.eq_symm_apply, map_mul] at fa fb

Goal state after:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

Tactic:
by
  simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (succ b)

Tactic:
by
  rw [Ico_succ_right_of_not_isMax hb, ← Ico_insert_right h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ insert (succ a) (Ioc (succ a) b) = Ioc a b

Tactic:
rw [Ioc_insert_left (succ_le_of_lt h), Icc_succ_left_of_not_isMax h.not_isMax]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Disjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
disjoint_def

Goal state after:
case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ∀ x ∈ (inl R M M₂).range, x ∈ (inr R M M₂).range → x = 0
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range

Tactic:
Submodule.range_subtype

Goal state after:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ g.ker ≤ f.range
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M₂
hx : x ∈ ↑p₂
⊢ (inr R M M₂) x ∈ p₁.prod p₂

Tactic:
exact ⟨zero_mem p₁, hx⟩

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f) i

Tactic:
· exact le_partialSups_of_le f hj_mem

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ i ≤ j

Tactic:
← iterate_succ_toZ i hi,

Goal state after:
case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ succ^[(toZ i0 i).toNat] i0 ≤ j
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets

Tactic:
intro x y a hx b hy

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
⊢ ∃ i, x ∩ y ∈ (f i).sets
Module: Mathlib.Order.Filter.AtTopBot.Disjoint

Goal state before:
pp: case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)
    exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge

Goal state after: