mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2) x) =
    (∏ x ∈ f1.support, g x (f1 x + f2 x)) * ∏ x ∈ f2.support, g x (f1 x + f2 x)

Tactic:
prod_union hd,

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (∏ x ∈ f1.support, g x ((f1 + f2) x)) * ∏ x ∈ f2.support, g x ((f1 + f2) x) =
    (∏ x ∈ f1.support, g x (f1 x + f2 x)) * ∏ x ∈ f2.support, g x (f1 x + f2 x)
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
s : List ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
induction s with
  | nil => simp
  | cons a s hind =>
    simp only [map_cons, prod_cons]
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    apply mul_le_mul
    · apply h
      simp
    · grind
    · grind [prod_nonneg]
    · apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulMono R
F : Type u_2
L : Type u_3
inst✝ : FunLike F L R
f : F
r : R
t : Multiset L
hf0 : ∀ (x : L), x ∈ t → 0 ≤ f x
hf : ∀ (x : L), x ∈ t → f x ≤ r
⊢ (map (⇑f) t).prod ≤ r ^ t.card

Tactic:
induction t using Quotient.inductionOn
  simp_all [List.prod_map_le_pow_length₀]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ (map f 0).prod

Tactic:
by simp [h_one]

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 : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' ↑l.support)
a : α
⊢ a ∈ l.support.preimage f hf ↔ l (f a) ≠ 0

Tactic:
Finset.mem_preimage

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 : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' ↑l.support)
a : α
⊢ f a ∈ l.support ↔ l (f a) ≠ 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α
c : γ
⊢ (single a c).sumElim 0 = single (Sum.inl a) c

Tactic:
classical ext (_ | _) <;> simp [single_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β
c : γ
⊢ sumElim 0 (single b c) = single (Sum.inr b) c

Tactic:
classical ext (_ | _) <;> simp [single_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddMonoid M
a : α
b : β
m₁ m₂ : M
⊢ (single a m₁).sumElim (single b m₂) = single (Sum.inl a) m₁ + single (Sum.inr b) m₂

Tactic:
classical ext (_ | _) <;> simp [single_apply]

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✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Tactic:
calc
    ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
      rw [← prod_union, filter_union_filter_not_eq]
      exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
    _ ≤ ∏ x ∈ t, f x :=
      mul_le_of_le_one_of_le
        (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
        (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])

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

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
rw [← l.sum_single]

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l.sum single ∈ span R ((fun i ↦ single i 1) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
x✝ : f a = 0
⊢ 0 • Pi.single a c a = 0

Tactic:
simp only [zero_smul]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
⊢ s ∩ mulSupport f = ↑hf.toFinset ∩ mulSupport f

Tactic:
by simp [inter_assoc]

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 : Basis ι R M
R₁ : Type u_13
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x

Tactic:
rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]

Goal state after:
ι : 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₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
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 : Basis ι R M
R₁ : Type u_13
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x

Tactic:
rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]

Goal state after:
ι : 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₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #{x | p x} = if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}

Tactic:
rw [Fin.univ_succ, filter_cons, apply_ite Finset.card, card_cons, filter_map, card_map]

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ) + 1
    else #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ)) =
    if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R

Tactic:
by
  refine .ofLinearMap (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_ <;>
  ext j k <;> obtain rfl | hk := eq_or_ne i k
  · simp [h₀]
  · simp [hk]
  · simp [h₀]
  · simp [hk]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport (f ∘ g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
· unfold Function.comp at hs
      rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
      rwa [image_inter_mulSupport_eq, infinite_image_iff hg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j

Tactic:
rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i < (finRotate n) i ↔ i ≠ -1

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]

Goal state after:
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
v : ι → M
hli : LinearIndependent R v
i : ι
⊢ (Basis.span hli) i = ⟨v i, ⋯⟩

Tactic:
by
  ext
  exact congr_arg ((↑) : span R (range v) → M) <| Basis.mk_apply _ _ _

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

Goal state before:
pp: case mp
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

pp: case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)

Tactic:
· rintro ⟨b⟩
    refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩
    simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq

Goal state after:
case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)
Module: Mathlib.Data.ENat.Pow

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

Tactic:
y_0,

Goal state after:
case refine_2
x y : ℕ∞
h : x ^ 0 = 0
y_0 : y = 0
⊢ False
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ m.toNat • p + a = b + (-m).toNat • p

Tactic:
← sub_eq_sub_iff_add_eq_add,

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ m.toNat • p - (-m).toNat • p = b - a
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : c ∣ b
⊢ (a + b).Coprime c ↔ a.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : c ∣ a
⊢ (a + b).Coprime c ↔ b.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : a ∣ c
⊢ a.Coprime (b + c) ↔ a.Coprime b

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
h : a ∣ b
⊢ a.Coprime (b + c) ↔ a.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a : Fin (0 ^ (n + 1))
⊢ ↑a / 0 ^ ↑b % 0 < 0

Tactic:
rw [zero_pow n.succ_ne_zero] at a

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a✝ : Fin (0 ^ (n + 1))
a : Fin 0
⊢ ↑a✝ / 0 ^ ↑b % 0 < 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
⊢ s = t

Tactic:
let f : t ↪ s :=
    ⟨fun x => ⟨x.1, h x.2⟩, fun a b hab => Subtype.coe_injective (Subtype.mk.inj hab)⟩

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ s = t
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
⊢ LinearIndependent R v →
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
intro h
    refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
    exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint

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

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
rw [this]
    split_ifs with h
    · 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]
    · rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]

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

Goal state before:
pp: a b c : ℕ
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
by_cases h : c = 0
  · simp [h]
  · rw [Nat.add_div (Nat.pos_of_ne_zero h), Nat.add_le_add_iff_left]
    split <;> decide

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

Goal state before:
pp: α : Type u_3
⊢ card α = 0 ↔ IsEmpty α

Tactic:
← Cardinal.mk_eq_zero_iff

Goal state after:
α : Type u_3
⊢ card α = 0 ↔ #α = 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ Module.rank R M

Tactic:
by
  simpa using hv.cardinal_lift_le_rank

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

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑n < #↑↑s
⊢ ∃ s, s.card = n + 1 ∧ LinearIndepOn R id ↑s

Tactic:
rw [← natCast_add_one_le_iff, ← Nat.cast_add_one] at le

Goal state after:
case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
⊢ ∃ s, s.card = n + 1 ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ i ∈ t₁ᶜ, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
· rw [← Finset.sum_subset ht₁t₂.le_compl_left]
      · convert! heq using 2 with i hi i hi <;> simp [hi]
      · intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R → R'
j : M ≃+ M₁
hi : Bijective i
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ Module.rank R M = Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hi hc

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

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

Tactic:
rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]

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

Goal state before:
pp: α : Type u_1
a : α
this : Disjoint {x | x ≠ a} {a}
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
replace this := (Set.encard_union_eq this).symm

Goal state after:
α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
⊢ {x | x ≠ a}.encard + 1 = ENat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
rw [ncard_insert_of_mem h, if_pos h]

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

Goal state before:
pp: α : Type u_1
a b : α
h : a ≠ b
⊢ {a, b}.ncard = 2

Tactic:
by
  simp [h]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
obtain hs | hs := s.finite_or_infinite
  · apply ncard_le_ncard sdiff_subset hs
  convert! Nat.zero_le _
  exact (hs.sdiff (by simp)).ncard

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = n

Tactic:
by
    rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
    exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ StrictMono fun t ↦ (Subgroup.comap s.subtype t, mk '' ↑t)

Tactic:
by
  refine fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩,
    mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩
  obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩
  convert t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x : α ⧸ s
⊢ MulAction.orbitRel.Quotient.orbit x = Quotient.out x • ↑s

Tactic:
induction x using QuotientGroup.induction_on

Goal state after:
case H
α : Type u_1
inst✝ : Group α
s : Subgroup α
z✝ : α
⊢ MulAction.orbitRel.Quotient.orbit ↑z✝ = Quotient.out ↑z✝ • ↑s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
by
  obtain ht | ht := t.finite_or_infinite
  · exact ncard_sdiff' hst ht
  · rw [ht.ncard, Nat.zero_sub, (ht.sdiff hs).ncard]

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
r : R
⊢ (↑↑(f.prod g.toRingHom)).toFun ((algebraMap R A) r) = (algebraMap R (B × C)) r

Tactic:
simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom,
        commutes, Prod.algebraMap_apply]

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

Goal state before:
pp: A : Type u
inst✝ : CommGroup A
n : ℤ
⊢ MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Tactic:
ext x
  rw [← Quotient.out_eq' x]
  rfl

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

Goal state before:
pp: A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Tactic:
ext x
  rw [← Quotient.out_eq' x]
  rfl

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
rw [SetLike.ext_iff] at he₁ he₂

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : ∀ (x : H × I), x ∈ mrange f ↔ x ∈ e₁.mgraph
e₂ : I →* H
he₂ : ∀ (x : I × H), x ∈ mrange (MulEquiv.prodComm.toMonoidHom.comp f) ↔ x ∈ e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h