mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

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
inst✝ : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), x ∈ supported M R (s ∪ t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
simpa [Finsupp.mem_supported, Finsupp.support_single _ hx] using h (Finsupp.single a x)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : SMulCommClass R R S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
i : ι
n : ↥N
⊢ (mulLeftMap N m) (single i n) = ↑(m i) * ↑n

Tactic:
by
  simp [mulLeftMap]

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
hx : x ∈ (linearCombination R v).range
⊢ x ∈ span R (Set.range v)

Tactic:
rw [LinearMap.mem_range] at hx

Goal state after:
case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
hx : ∃ y, (linearCombination R v) y = x
⊢ x ∈ span R (Set.range v)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down)

Tactic:
HasFiniteMulSupport,

Goal state after:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬(mulSupport ((fun i ↦ f i) ∘ PLift.down)).Finite
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (linearCombination R ⇑b) (b.repr x) = x

Tactic:
rw [← b.coe_repr_symm]
  exact b.repr.symm_apply_apply x

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
rw [← mulSupport_mulIndicator] at hf hg

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Tactic:
biUnion_eq_iUnion,

Goal state after:
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝ : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype ↑I
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x, t ↑x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (a, a_1) ∈ {x ∈ s | x.1 = a}

case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ {x ∈ s | x.1 = a}, a_1.2 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})

case refine_3
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), (a, a_1).2 = a_1

case refine_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ {x ∈ s | x.1 = a}, (a, a_1.2) = a_1

case refine_5
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
a : α
⊢ ∀ a_1 ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, a_1) = f (a, a_1)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1

Tactic:
cases i
      simp only [Fin.lt_def, Fin.val_last] at h
      simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

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
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (⇑b '' s)
⊢ ↑(b.repr m).support ⊆ s

Tactic:
by
  rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩
  rwa [repr_linearCombination, ← Finsupp.mem_supported R l]

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

Goal state before:
pp: x y : ℕ∞
h : x = 1 ∨ y = 0
⊢ x ^ y = 1

Tactic:
rcases h with h | h

Goal state after:
case inl
x y : ℕ∞
h : x = 1
⊢ x ^ y = 1

case inr
x y : ℕ∞
h : y = 0
⊢ x ^ y = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inl
x y z : ℕ∞
x_2 : 1 < x
y_0 : y < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
simp only [Order.lt_one_iff.1 y_0, mul_zero, zero_epow_top]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
⊢ LinearIndependent R v

Tactic:
intro x y hxy
  let f := fun r : R => r • (1 : K)
  have := @li (x.mapRange f (by simp [f])) (y.mapRange f (by simp [f])) ?_
  · ext i
    exact hinj congr($this i)
  simpa [Finsupp.linearCombination, f, Finsupp.sum_mapRange_index]

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

Goal state before:
pp: case inl
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
H : i = j
right✝ : c = d
⊢ i = j

Tactic:
exact 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)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
⊢ ∃ a, f a = i

Tactic:
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]

Goal state after:
ι : 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)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
⊢ ∃ a, f a = i
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
rcases m with - | m

Goal state after:
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

case succ.succ
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
m : ℕ
a : Fin ((m + 1) ^ (n + 1))
⊢ ↑a / (m + 1) ^ ↑b % (m + 1) < m + 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m) ∧
    ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)

Tactic:
constructor <;> rw [Int.emod_def, ← sub_add] <;>
            refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

case left.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑n ∣ ↑(n.lcm m)

case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

case right.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑(n.lcm m)
Module: Mathlib.LinearAlgebra.Dimension.Basic

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

Tactic:
exact ⟨_, s_ind.comp _ (s.equivFinOfCardEq s_card).symm.injective⟩

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

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

Tactic:
toFinset_card

Goal state after:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = ↑(Fintype.card ↑s)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard

Tactic:
← union_sdiff_cancel h,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ (s ∪ t \ s).encard
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ LinearIndependent K v ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
apply linearIndependent_iff_eq_zero_of_smul_mem_span.trans

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ card α = ↑(Nat.card α)

Tactic:
unfold ENat.card

Goal state after:
α : Type u_4
inst✝ : Finite α
⊢ Cardinal.toENat (Cardinal.mk α) = ↑(Nat.card α)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = s.toFinset.card

Tactic:
toFinset_card

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card ↑s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ (f ⁻¹' s).ncard = s.ncard

Tactic:
by
  rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
by
  have := hs.to_subtype
  obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k
  refine ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), ?_⟩
  rw [ncard_image_of_injective _ Subtype.coe_injective]
  simp

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

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

Tactic:
rw [Ico_succ_right_of_not_isMax hb, ← Ico_insert_right h]

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
q : Submodule R M₂
⊢ p.prod q = map id (p.prod q)

Tactic:
map_id

Goal state after:
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
q : Submodule R M₂
⊢ p.prod q = p.prod q
Module: Mathlib.Data.Fintype.Pigeonhole

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
val✝ : Fintype β
key : Fintype α := { elems := univ.biUnion fun y ↦ (f ⁻¹' {y}).toFinset, complete := ⋯ }
⊢ False

Tactic:
exact key.false

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 α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
  exact Set.image_add_const_Ioc _ _ _

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
⊢ IsMax i

Tactic:
refine fun j _ ↦ not_lt.mp fun hij_lt ↦ ?_

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst

Tactic:
refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_ <;> simp

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

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

Tactic:
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ _) (Int.toNat_le_toNat h_le)

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ IsCompactElement ⊤

Tactic:
by
  simpa only [← span_singleton_one] using Submodule.singleton_span_isCompactElement 1

Goal state after:
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:
rw [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: case mpr
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ a, ∃ b ∈ I, a * y + b = x) → ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x

Tactic:
rintro ⟨a, b, hb, rfl⟩
    exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, -y} = span {x, y}

Tactic:
rw [span_pair_comm, span_insert_neg, span_pair_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
⊢ (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)

Tactic:
rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ ij ∈ antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 =
    (∏ ij ∈ antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) *
      ∏ ij ∈ antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2

Tactic:
by
  simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
  have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
  congr 1
  · refine prod_congr rfl fun i hi ↦ ?_
    rw [tsub_add_eq_add_tsub (this _ hi)]
  · refine prod_congr rfl fun i hi ↦ ?_
    rw [choose_symm (this _ hi)]

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 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : ∃ x ∈ ↑f.support, (f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))

Tactic:
rcases hx with ⟨x, _, rfl⟩

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)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ (f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (∑ x_1 ∈ x.support, (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (x x_1)).1 = x 0

Tactic:
Prod.fst_sum

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ ∑ c ∈ x.support, ((((inr R P M ∘ₗ f) ^ c) ∘ₗ inl R P M) (x c)).1 = x 0
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ {y | ∀ ⦃x_1 : β⦄, x = y.1 ∧ x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
and_imp,

Goal state after:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ {y | ∀ ⦃x_1 : β⦄, x = y.1 → x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c

Tactic:
by_cases h : c ∈ s <;> simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ map id F = F

Tactic:
map_id

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ F = F
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ map id F = F

Tactic:
map_id

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ F = F
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map id g

Tactic:
map_id

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ g
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
⊢ (iInf f).NeBot

Tactic:
by
  cases isEmpty_or_nonempty ι
  · constructor
    simp [iInf_of_empty f, top_ne_bot]
  · exact iInf_neBot_of_directed' hd hb

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

Goal state before:
pp: α : Type u
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f

Tactic:
simp only [← le_principal_iff, (isCompl_principal s).le_left_iff, disjoint_assoc, inf_principal,
    ← (isCompl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
⊢ ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s

Tactic:
ext
  simp only [mem_iSup, mem_inf_principal]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0

Tactic:
by simpa using ((EventuallyEq.refl l f).sub h).symm

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommMonoid α

Tactic:
apply e.injective.commMonoid _

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.Group.TransferInstance

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

Tactic:
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.group _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝¹ : AddZeroClass B
inst✝ : DistribSMul M B
⊢ DistribSMul M A

Tactic:
letI := e.addZeroClass

Goal state after:
M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝¹ : AddZeroClass B
inst✝ : DistribSMul M B
this : AddZeroClass A := e.addZeroClass
⊢ DistribSMul M A
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : Nonempty α
s : Set α
hs : IsCofinal s
⊢ s.Nonempty

Tactic:
inhabit α

Goal state after:
α : Type u_1
inst✝¹ : LE α
inst✝ : Nonempty α
s : Set α
hs : IsCofinal s
inhabited_h : Inhabited α
⊢ s.Nonempty