mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by have := b.isTorsionFree; exact smul_eq_zero

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
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ Injective ⇑(Fintype.linearCombination R v)

Tactic:
by
  simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]

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

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
⊢ 1 ^ y = 1

Tactic:
one_pow

Goal state after:
case coe
y✝ : ℕ∞
y : ℕ
⊢ 1 = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
⊢ x ^ ⊤ = ⊤

Tactic:
by
  have : (0 : ℕ∞) ≤ 1 := zero_le_one
  rw [epow_def, if_neg, if_neg, if_neg] <;> grind

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

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y

Tactic:
simpa using epow_right_mono h zero_le

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ uIcc a.succ b.succ, f i = ∏ i ∈ uIcc a b, f i.succ

Tactic:
simp [← map_succEmb_uIcc]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inl
b c : ℕ
⊢ ((if c = 0 then 1 else 0) - 1) % ((if b = 0 then 1 else 0) - 1) = (if c % b = 0 then 1 else 0) - 1

Tactic:
split_ifs

Goal state after:
case pos
b c : ℕ
h✝² : c = 0
h✝¹ : b = 0
h✝ : c % b = 0
⊢ (1 - 1) % (1 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : c = 0
h✝¹ : b = 0
h✝ : ¬c % b = 0
⊢ (1 - 1) % (1 - 1) = 0 - 1

case pos
b c : ℕ
h✝² : c = 0
h✝¹ : ¬b = 0
h✝ : c % b = 0
⊢ (1 - 1) % (0 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : c = 0
h✝¹ : ¬b = 0
h✝ : ¬c % b = 0
⊢ (1 - 1) % (0 - 1) = 0 - 1

case pos
b c : ℕ
h✝² : ¬c = 0
h✝¹ : b = 0
h✝ : c % b = 0
⊢ (0 - 1) % (1 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : ¬c = 0
h✝¹ : b = 0
h✝ : ¬c % b = 0
⊢ (0 - 1) % (1 - 1) = 0 - 1

case pos
b c : ℕ
h✝² : ¬c = 0
h✝¹ : ¬b = 0
h✝ : c % b = 0
⊢ (0 - 1) % (0 - 1) = 1 - 1

case neg
b c : ℕ
h✝² : ¬c = 0
h✝¹ : ¬b = 0
h✝ : ¬c % b = 0
⊢ (0 - 1) % (0 - 1) = 0 - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
· suffices a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1) by
      rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
    rw [← Nat.add_sub_assoc (one_le_pow (c - b) a ha0), ← mul_add_one, pow_add,
      Nat.sub_add_cancel (one_le_pow b a ha0)]

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

Goal state before:
pp: n a b : ℕ
⊢ ↑b % ↑n = ↑a % ↑n ↔ ↑n ∣ ↑b - ↑a

Tactic:
Int.emod_eq_emod_iff_emod_sub_eq_zero,

Goal state after:
n a b : ℕ
⊢ (↑b - ↑a) % ↑n = 0 ↔ ↑n ∣ ↑b - ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b : ℕ
⊢ a = b % 0 ↔ a = b

Tactic:
mod_zero

Goal state after:
a b : ℕ
⊢ a = b ↔ a = b
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
h : 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:
refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩

Goal state after:
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
h : LinearIndependent R v
⊢ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)

Tactic:
convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]

Goal state after:
case e'_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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with g i ≤ f i, f i • v i + ∑ i ∈ s with f i < g i, f i • v i

case e'_3
ι : 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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ i ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x) =
    ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, g i • v i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i = ∏ i, (g :: h :: L)[i] ^ (-1) ^ ↑i

Tactic:
by
        { rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
          simp [pow_add]}

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

Goal state before:
pp: case neg
ι : 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 : Finset ι
f : ι → R
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hi : i ∉ t
⊢ f i = 0

Tactic:
exact h.2 i (Finset.mem_compl.2 hi)

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

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

Tactic:
rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2

Goal state after:
case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : card β < 1
⊢ card (α → β) = card β ^ ⊤

case inr.inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) = card β ^ ⊤

case inr.inr.inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_2 : 1 < card β
⊢ card (α → β) = card β ^ ⊤
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, ?_⟩

Goal state after:
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
⊢ LinearIndepOn R id ↑(Finset.map { toFun := v, inj' := ⋯ } Finset.univ)
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < Module.rank R M

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]
  · exact natCast_lt_aleph0
  · contrapose! h
    rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
    exact n.zero_le

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k

Tactic:
ENat.le_natCast_iff

Goal state after:
α : Type u_1
s : Set α
k : ℕ
h : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
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} (⨆ ι, #↑↑ι)

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
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?b

pp: case b
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.{max v' v}

Tactic:
· apply Cardinal.lift_le.mpr
    refine le_ciSup Cardinal.bddAbove_of_small ⟨rangeSplitting f '' s, ?_⟩
    apply LinearIndependent.of_comp f.rangeRestrict
    convert! li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1

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
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} #↑↑⟨rangeSplitting ⇑f '' s, ⋯⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.Finite ↔ t.Finite

Tactic:
rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ f, ∑ i ∈ s, f i • v i = 0 ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
by
  simpa using linearIndepOn_finset_iff.not

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
h : ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
f : ι →₀ R
hf : f ∈ Finsupp.supported R R s
g : ι →₀ R
hg : g ∈ Finsupp.supported R R s
eq : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
⊢ (Finsupp.linearCombination R v) (f - g) = 0

Tactic:
by rw [map_sub, eq, sub_self]

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ Finsupp.single i (l i) - l ∈ Finsupp.supported R R (univ \ {i})

Tactic:
Finsupp.mem_supported'

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ ∀ x ∉ univ \ {i}, (Finsupp.single i (l i) - l) x = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = k

Tactic:
by
  induction k using ENat.nat_induction with
  | zero => exact ⟨∅, empty_subset _, by simp⟩
  | succ n IH =>
    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
    simp only [Nat.cast_succ] at *
    have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
    obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
    exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩

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

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
⊢ ∀ (c : R), ∀ y ∈ span R (range (Subtype.val ∘ v)), c • x + y = 0 → c = 0

Tactic:
intro c y hy hc

Goal state after:
case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
c : R
y : M
hy : y ∈ span R (range (Subtype.val ∘ v))
hc : c • x + y = 0
⊢ c = 0
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ ↑l.length ≤ ENat.card α

Tactic:
cases finite_or_infinite α
  · grw [h.length_le_natCard, ENat.card_eq_coe_natCard]
  · grw [ENat.card_eq_top_of_infinite]
    exact le_top

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
h : s.Finite
h✝ : a ∈ s
⊢ s.ncard ≤ s.ncard

case neg
α : Type u_1
a : α
s : Set α
h : s.Finite
h✝ : a ∉ s
⊢ s.ncard ≤ s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard

Tactic:
simp only [← Nat.not_even_iff_odd, Nat.not_even_one, iff_false, Decidable.not_not]

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

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

Tactic:
by
  rw [finite_iff_subgroup_quotient]; constructor <;> assumption

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α ⧸ ⊥
⊢ ↑(Quotient.lift id ⋯ x) = x

Tactic:
by induction x using Quotient.inductionOn; simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
R : Type u_3
inst✝ : AddGroupWithOne R
hst : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard = ↑t.ncard - ↑s.ncard

Tactic:
by
  rw [ncard_sdiff hst (ht.subset hst), Nat.cast_sub (ncard_le_ncard hst ht)]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ s.ncard + (t \ s).ncard

Tactic:
by rw [add_comm]; apply ncard_le_ncard_sdiff_add_ncard _ _ hs

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
ext x
    rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂)
⊢ p₁.prod p₂ ≤ q ↔ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q

Tactic:
by
  constructor
  · intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, zero_mem p₂⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨zero_mem p₁, hx⟩
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1
    have h2' : (LinearMap.inr R _ _) x2 ∈ q := by
      apply hK
      simpa using h2
    simpa using add_mem h1' h2'

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
intro x y
    rw [hp]
    rfl

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ sSup (Set.range fun i ↦ (partialSups f) i) = sSup ∅

Tactic:
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)

Goal state after:
case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ sSup ∅ = sSup ∅
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ico a b) (Ico (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iio]
  exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => lt_of_add_lt_add_right hx.2

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
Icc_eq_cons_Ico h,

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ cons b (Ico a b) ⋯, f x
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x > a, f x = ∏ x ≥ a, f x

Tactic:
mul_prod_Ioi_eq_prod_Ici

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ ∏ x ≥ a, f x = ∏ x ≥ a, f x
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + z * y, y} = span {x, y}

Tactic:
by
  rw [mul_comm, span_pair_add_right_mul]

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

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ^ (f.support.card * n + 1) ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
one_pow

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
α : Type u_3
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
a : α
inst✝ : Subsingleton α
m : M
b : α
⊢ ((uniqueLinearEquiv R M a).symm m) b = m

Tactic:
by simp [Subsingleton.elim b a]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
⊢ l.HasBasis (fun i ↦ p i ∧ q i) s

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f

Tactic:
exact image_mem_map univ_mem

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x : α
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
rcases hs x with ⟨y, ys, hy⟩

Goal state after:
case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
⊢ Ici x ∈ (generate (Ici '' s)).sets
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case h
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
i : ι
⊢ Iio (f i) ⊆ Iic (f i)

Tactic:
exact Iio_subset_Iic_self

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

Goal state before:
pp: case h
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
i : ι
⊢ Iio (f i) ⊆ Iic (f i)

Tactic:
exact Iio_subset_Iic_self

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
x : α
⊢ (l ⊔ pure x).HasBasis p fun i ↦ s i ∪ {x}

Tactic:
by
  simp only [← principal_singleton, hl.sup_principal]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ ¬⊥.NeBot ↔ ¬(f.NeBot ∧ Nonempty β)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ¬⊥.NeBot ↔ ¬(Nonempty α ∧ f.NeBot)