mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ ∀ (a b c : Fin n), a + b + c = a + (b + c)

Tactic:
by simp [add_def, Nat.add_assoc]

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

Goal state before:
pp: case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
    rfl

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

Goal state before:
pp: case pos
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : Even n
⊢ 0 + (-1) ^ n = 1

Tactic:
simp [*]

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

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

Tactic:
by
  simp only [LinearIndepOn, linearIndependent_iffₛ, Finsupp.mem_supported,
    Finsupp.linearCombination_apply, Set.subset_def, Finset.mem_coe]
  refine ⟨fun h l₁ h₁ l₂ h₂ eq ↦ (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <| h _ _ <|
    (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
    fun h l₁ l₂ eq ↦ ?_⟩
  refine Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_
  iterate 2 simpa using fun _ h _ ↦ h
  simp_rw [Finsupp.embDomain_eq_mapDomain]
  rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index] <;>
    intros <;> simp only [zero_smul, add_smul]

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

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ ↑n ∣ ↑b - ↑a ↔ ↑n ∣ ↑(b - a)

Tactic:
Int.ofNat_sub h

Goal state after:
n a b : ℕ
h : a ≤ b
⊢ ↑n ∣ ↑b - ↑a ↔ ↑n ∣ ↑b - ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b : ℕ
h : b ≤ a
⊢ ↑(a - b) ∣ ↑a - ↑b

Tactic:
Int.ofNat_sub h

Goal state after:
a b : ℕ
h : b ≤ a
⊢ ↑a - ↑b ∣ ↑a - ↑b
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ [g].alternatingProd = ∏ i, [g][i] ^ (-1) ^ ↑i

Tactic:
change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ g = ∏ i, [g][i] ^ (-1) ^ ↑i
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Bijective f ↔ Injective f ∧ Fintype.card α = Fintype.card β

Tactic:
Fintype.bijective_iff_injective_and_card

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Injective f ∧ Fintype.card α = Fintype.card β ↔ Injective f ∧ Fintype.card α = Fintype.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
⊢ card α = ⊤ ↔ Infinite α

Tactic:
by simp [card, aleph0_le_mk_iff]

Goal state after:
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
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
t : Finset ↑↑s
ht : n + 1 = t.card
⊢ (Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t).card = n + 1

Tactic:
by simpa using ht.symm

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 3
hx : x ∈ s
⊢ 3 = 2 + 1

Tactic:
by exact rfl

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
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ g, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
simpa using not_iff_not.2 Fintype.linearIndependent_iff

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 4
hx : x ∈ s
⊢ 4 = 3 + 1

Tactic:
by exact rfl

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

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
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ P ↔ ∃ c, x = c.sum fun i x ↦ x • ↑(b i)

Tactic:
conv_lhs =>
    rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
        ← Finsupp.range_linearCombination]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ (linearCombination R (⇑P.subtype ∘ ⇑b)).range ↔ ∃ c, x = c.sum fun i x ↦ x • ↑(b i)
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
sum_eq : ∑ i, g i • (Subtype.val ∘ fun x_1 ↦ ⟨x, hx⟩) i = 0
i : Fin 1
⊢ g i = 0

Tactic:
simp only [Fin.default_eq_zero, Finset.univ_unique,
    Finset.sum_singleton] at sum_eq

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
i : Fin 1
sum_eq : g 0 • (Subtype.val ∘ fun x_1 ↦ ⟨x, hx⟩) 0 = 0
⊢ g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).ncard ≤ s.ncard + 1

pp: case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
· to_encard_tac; rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]; apply encard_insert_le

Goal state after:
case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1
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
x y : G × H
⊢ x ∈ {x | f x.1 = x.2} → y ∈ {x | f x.1 = x.2} → x * y ∈ {x | f x.1 = x.2}

Tactic:
by simp +contextual

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✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : G →* H
x : G × H
⊢ x ∈ f.mgraph.carrier → x⁻¹ ∈ f.mgraph.carrier

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ ((fun f ↦ ∑ i, f i ∘ₗ proj i) ((fun f i ↦ f ∘ₗ single R φ i) f)) x = f x

Tactic:
suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]

Goal state after:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ f (∑ j, Pi.single j (x j)) = f x
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x : M₃
⊢ x ∈ (f.coprod g).range ↔ x ∈ f.range ⊔ g.range

Tactic:
simp [mem_sup]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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

Tactic:
simp [*]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
⊢ ↑(Iic (pred b)) = ↑(Iio b)

Tactic:
simpa using Set.Iic_pred_eq_Iio_of_not_isMin hb

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
k : ι'
⊢ x (Sum.inr k) = 0

pp: case refine_2
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
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
· induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]

Goal state after:
case refine_2
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
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (partialSups f) i = ⨆ i_1, f ↑i_1

Tactic:
simp only [partialSups_apply]
  apply le_antisymm
  · exact sup'_le _ _ fun j hj ↦ Finite.le_ciSup_of_le
      ⟨j, by simpa only [Set.mem_Iic, mem_Iic] using hj⟩ le_rfl
  · exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i = j
⊢ ∃ n, succ^[n] i = j

Tactic:
refine ⟨0, ?_⟩

Goal state after:
case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i = j
⊢ succ^[0] i = j
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case mp
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 a b : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
⊢ a + b = n → a ≤ n ∧ b = n - a

pp: case mpr
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 a b : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
⊢ a ≤ n ∧ b = n - a → a + b = n

Tactic:
· rintro rfl
    exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩

Goal state after:
case mpr
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 a b : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
⊢ a ≤ n ∧ b = n - a → a + b = n
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range (n + 1)) =
    map (fun i ↦ (i, n - i)) (map (fun x ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))

Tactic:
map_map

Goal state after:
n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range (n + 1)) =
    map ((fun i ↦ (i, n - i)) ∘ fun x ↦ 0 + (n + 1) - 1 - x) (range (n + 1))
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_3.e'_6
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = if hi : ↑a < n + 1 then f ⟨↑a, hi⟩ else 1

Tactic:
simp only [Order.lt_add_one_iff, is_le', ↓reduceDIte]
    rfl

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map { toFun := Prod.swap, inj' := ⋯ } (map { toFun := fun i ↦ (i, n - i), inj' := ⋯ } (range (n + 1))) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
map_map

Goal state after:
n : ℕ
⊢ map ({ toFun := fun i ↦ (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (n + 1, 0))
        (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Tactic:
map_map

Goal state after:
n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (n + 1, 0))
        (map
          (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }).trans
            ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
          (antidiagonal n))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding
      (map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)

Tactic:
map_map

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map (({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding)
      (antidiagonal k) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding
      (map ({ toFun := fun x ↦ x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
map_map

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map (({ toFun := fun x ↦ x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding)
      (antidiagonal (n - k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d ∈ I

Tactic:
rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]

Goal state after:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ k ∈ range n.succ, n.choose k • (x ^ k * y ^ (n - k))

Tactic:
nsmul_eq_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ x_1 ∈ range n.succ, ↑(n.choose x_1) * (x ^ x_1 * y ^ (n - x_1))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ (if n = 0 then 1 else 0) = 0

Tactic:
if_neg h0

Goal state after:
n : ℕ
h0 : n ≠ 0
⊢ 0 = 0
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ univ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
inst✝ : f.NeBot
⊢ (f ⊔ g).NeBot

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
inst✝ : g.NeBot
⊢ (f ⊔ g).NeBot

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
⊢ p s

Tactic:
have C : ∀ i, ∀ s ∈ f i, q s := fun i s hs ↦
    ⟨mem_iInf_of_mem _ hs, fun t hst ↦ p_of_f _ _ (mem_of_superset hs hst)⟩

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
⊢ p s
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
⊢ l = ⊤

Tactic:
refine top_unique fun s hs => ?_

Goal state after:
α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
s : Set α
hs : s ∈ l
⊢ s ∈ ⊤
Module: Mathlib.Order.Filter.AtTopBot.Disjoint

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
⊢ Disjoint atBot atTop

Tactic:
rcases exists_pair_ne α with ⟨x, y, hne⟩
  by_cases hle : x ≤ y
  · 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
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
    exact Iic_disjoint_Ici.2 hle

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ g ≤ map mab f

Tactic:
rw [← @map_id _ g, ← map_congr h₁, ← map_map]
  exact map_mono h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ map f (map g x) ≤ y ↔ map (f ∘ g) x ≤ y

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ map (f ∘ g) x ≤ y ↔ map (f ∘ g) x ≤ y
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
c : Filter γ
h : Tendsto (g ∘ f) a c
⊢ map g (map f a) ≤ c

Tactic:
map_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
c : Filter γ
h : Tendsto (g ∘ f) a c
⊢ map (g ∘ f) a ≤ c
Module: Mathlib.Order.Filter.Map

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

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : ¬p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
x✝ : Set (π' (f a))
⊢ Sigma.mk a '' g a ⁻¹' id x✝ = Sigma.map f g ⁻¹' Sigma.mk (f a) '' id x✝

Tactic:
apply image_sigmaMk_preimage_sigmaMap hf

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
⊢ CommGroup α

Tactic:
by
  let one := e.one
  let mul := e.mul
  let inv := e.Inv
  let div := e.div
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  apply e.injective.commGroup _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ (k * b + (k - 1)) / k

Tactic:
rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]; lia

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩

Tactic:
← Subtype.coe_mk (p := (· ⊆ S)) _ hS0

Goal state after:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂

Tactic:
by rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Tactic:
by rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Goal state after: