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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ ⨆ i, f i x = 1

Tactic:
simp only [hx, ciSup_const]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

pp: case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
· rw [mulIndicator_of_mem hx]
    rw [mem_iUnion] at hx
    refine le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)
    rcases hx with ⟨i, hi⟩
    exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0

Tactic:
← add_sum_erase' _ a _ (fun _ ↦ rfl),

Goal state after:
α : Type u_1
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : (d a + (erase a d).sum fun x n ↦ n) = 1
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0

Tactic:
by rw [Pi.smul_apply', hf, zero_smul]

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

Goal state before:
pp: case pos
α : 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 : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
simp [hs0]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ (∀ (x : Subtype p), (subtypeDomain p f) x = (subtypeDomain p g) x) ↔ ∀ (x : α), p x → f x = g x

Tactic:
subtypeDomain_apply,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ (∀ (x : Subtype p), f ↑x = g ↑x) ↔ ∀ (x : α), p x → f x = g x
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:
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:
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:
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✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
⊢ mapDomain Sum.swap (f.sumElim g) = g.sumElim f

Tactic:
by
  simp [sumElim_eq_add, mapDomain_add, ← mapDomain_comp, Function.comp_def, add_comm]

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 ∈ insert i s, f j ≤ ∏ j ∈ t, f j

Tactic:
by
      apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    ∀ (x : β), x = z ∨ x ∈ i → ∀ (y : β), y = z ∨ y ∈ i → x ≠ y → Disjoint (f x) (f y)

Tactic:
forall_eq_or_imp,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    ((z ≠ z → Disjoint (f z) (f z)) ∧ ∀ a ∈ i, z ≠ a → Disjoint (f z) (f a)) ∧
      ∀ a ∈ i, (a ≠ z → Disjoint (f a) (f z)) ∧ ∀ a_2 ∈ i, a ≠ a_2 → Disjoint (f a) (f a_2)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Icc ↑i ↑j ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans_lt j.is_lt

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ioc ↑i ↑j ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans_lt j.is_lt

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
⊢ HasFiniteSupport f

Tactic:
cases subsingleton_or_nontrivial R
  · simp_rw [HasFiniteSupport, Subsingleton.support_eq, finite_empty]
  · apply hasFiniteSupport_of_finsum_ne_zero
    rw [h]
    exact one_ne_zero

Goal state after:
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
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), g (v i) = v' (f i)
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v

Tactic:
ext l
  simp [linearCombination_apply, h]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Ico i j = Ico (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Ico_natAdd, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioc i j = Ioc (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Ioc_natAdd, image_preimage_eq_of_subset]
  exact Ioc_subset_Ioi_self.trans <| image_natAdd_Ioi m i ▸ image_subset_range _ _

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

Goal state before:
pp: case refine_2
α : 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✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ x ∈ span R (v '' s)

Tactic:
rw [← hx]
    exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (finSuccEquiv' i) i = none

Tactic:
simp [finSuccEquiv']

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

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

Tactic:
obtain ⟨i, hi⟩ := i
    simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (fun a ↦ (a / n, Fin.ofNat n a)) ((fun p ↦ p.1 * n + ↑p.2) p) = p

Tactic:
by
    refine Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
    dsimp only
    rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]

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

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

Tactic:
rev_add,

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

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

Tactic:
rev_add,

Goal state after:
n : ℕ
a b : Fin n
⊢ a.rev < b.rev.rev ↔ a.rev < a.rev - b
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]

Tactic:
rw [modEq_iff_dvd] at *
  exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
⊢ Surjective ⇑f

Tactic:
intro i
  let repr : (span R (range (v ∘ f)) : Type _) → ι' →₀ R := (hv.comp f f.injective).repr
  let l := (repr ⟨v i, hss (mem_range_self i)⟩).mapDomain f
  have h_total_l : Finsupp.linearCombination R v l = v i := by
    dsimp only [l]
    rw [Finsupp.linearCombination_mapDomain]
    rw [(hv.comp f f.injective).linearCombination_repr]
  have h_total_eq : Finsupp.linearCombination R v l = Finsupp.linearCombination R v
       (Finsupp.single i 1) := by
    rw [h_total_l, Finsupp.linearCombination_single, one_smul]
  have l_eq : l = _ := hv h_total_eq
  dsimp only [l] at l_eq
  rw [← Finsupp.embDomain_eq_mapDomain] at l_eq
  rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with
    ⟨i', hi'⟩
  use i'
  exact hi'.2

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : j (∑ x ∈ S, i (r' x) • v x) = 0
⊢ r' s = 0

Tactic:
exact hi _ <| hv _ _ (hj _ H) s hs

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

Goal state before:
pp: a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ False

Tactic:
have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)

Goal state after:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
this : (a + b) % c = a % c + b % c
⊢ False
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ ↑1 < toENat #α

Tactic:
simp only [ENat.card, Nat.cast_one]

Goal state after:
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
inst✝ : Subsingleton R
⊢ toNat (Module.rank R M) = 1

Tactic:
rank_subsingleton,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ toNat 1 = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : t.encard ≤ s.encard
⊢ s = t

Tactic:
by
  rw [← zero_add (a := encard s), ← encard_sdiff_add_encard_of_subset hst] at hts
  have hdiff :=
    (ENat.addLECancellable_of_lt_top (ht.subset hst).encard_lt_top).add_le_add_iff_right.mp hts
  rw [nonpos_iff_eq_zero, encard_eq_zero, sdiff_eq_empty] at hdiff
  exact hst.antisymm hdiff

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

Goal state before:
pp: α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + 1 ≤ t₀.encard
⊢ False

Tactic:
ht₀,

Goal state after:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + 1 ≤ ↑n
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ↑s.encard.toNat = s.encard

Tactic:
ENat.natCast_toNat_eq_self,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.encard ≠ ⊤
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑(t \ s ∪ s) ≤ 0 + ENat.card ↑s

Tactic:
sdiff_union_of_subset hsub.subset

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑t ≤ 0 + ENat.card ↑s
Module: Mathlib.SetTheory.Cardinal.NatCard

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

pp: case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ENat.card α

Tactic:
· grw [h.length_le_natCard, ENat.card_eq_coe_natCard]

Goal state after:
case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ENat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
⊢ s.ncard = t.ncard

Tactic:
set f' : s → t := fun x ↦ ⟨f x.1 x.2, h₁ _ _⟩
  have hbij : f'.Bijective := by
    constructor
    · rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
      simp only [f', Subtype.mk.injEq] at hxy ⊢
      exact h₂ _ _ hx hy hxy
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := h₃ y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
  simp_rw [← _root_.Nat.card_coe_set_eq]
  exact Nat.card_congr (Equiv.ofBijective f' hbij)

Goal state after:
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:
obtain ht | ht := t.finite_or_infinite

Goal state after:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard

case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ (t \ s).ncard = t.ncard - s.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑(Quotient.out ↑a.2) ∈ t

Tactic:
out_eq'

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑a.2 ∈ t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
rcases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : IsEmpty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

case inr
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : Nonempty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom ≤ ringConGen (r on ⇑f)

Tactic:
rw [← comap_nonUnitalRingHomComp]
    simp

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1

Tactic:
by
  intro x hx
  apply existsUnique_of_exists_of_unique
  · exact hf.mul_inv_cancel hx
  · intro y z hxy hxz
    calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]

Goal state after:
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 : ι
⊢ proj i ∘ₗ single R φ j = diag j i

Tactic:
by
  rw [single_eq_pi_diag, proj_pi]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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₂
f : M →ₗ[R] M₂
I : Type u_1
x✝ : I → M₂
hx : x✝ ∈ Submodule.pi Set.univ fun x ↦ f.range
⊢ x✝ ∈ (f.compLeft I).range

Tactic:
choose y hy using hx
    exact ⟨fun i => y i trivial, funext fun i => hy i trivial⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2.inl
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι
⊢ x (Sum.inl i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inl i)

pp: case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)

Tactic:
· simp [single_apply]

Goal state after:
case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
by
  simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
by
  rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Goal state after:
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:
by
  rw [le_iff_exists_mul]
  use kl.2
  rwa [mem_mulAntidiagonal, eq_comm] at hlk

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup' ⋯ (disjointed t)

Tactic:
Finset.sup'_eq_sup,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup (disjointed t)
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b) ∈ antidiagonal n ∧ (a, b).1 = m ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
mem_antidiagonal,

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i ↦ Ico i b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma fun j ↦ Ico a (j + 1), f x.snd x.fst

Tactic:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]

Goal state after:
case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1 + 1

case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 + 1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 ≤ a_1 ∧ a_1 < b
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma (Ico a), f x.snd x.fst

Tactic:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]

Goal state after:
case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 + 1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1

case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 + 1 ≤ a_1 ∧ a_1 < b
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i) ∈ antidiagonal n

Tactic:
mem_antidiagonal,

Goal state after:
n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i).1 + (i, n - i).2 = n
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ x ∈ span {y} ⊔ I ↔ ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
Submodule.mem_sup

Goal state after:
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) ↔ ∃ a, ∃ b ∈ I, a * y + b = x
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x} ⊔ span {y} = span {x} ↔ x ∣ y

Tactic:
sup_eq_left,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {y} ≤ span {x} ↔ x ∣ y
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
by
  rw [mul_comm, span_pair_right_mul_add]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
rw [← RingHom.comp_apply]
  simp

Goal state after: