mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Iic i) = Iic (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Iio i) = Iio (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Icc i j) = Icc (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ico i j) = Ico (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ioc i j) = Ioc (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ioo i j) = Ioo (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (uIcc i j) = uIcc (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Ici i) = Ici (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Ioi i) = Ioi (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iic i) = Iic (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iio i) = Iio (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ici i) = Ici (natAdd m i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ioi i) = Ioi (natAdd m i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

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

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ici i) = Ici (natAdd m i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ioi i) = Ioi (natAdd m i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (fun x ↦ x.addNat m) (Ici i) = Ici (i.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioi i) = Ioi (i.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ici i) = Ici (i.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ioi i) = Ioi (i.addNat m)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image succ (Iic i) = Ioc 0 i.succ

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image succ (Iio i) = Ioo 0 i.succ

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (succEmb n) (Iic i) = Ioc 0 i.succ

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (succEmb n) (Iio i) = Ioo 0 i.succ

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Icc i j) = Icc j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ico i j) = Ioc j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ioc i j) = Ico j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ioo i j) = Ioo j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (uIcc i j) = uIcc i.rev j.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Icc i j) = Icc j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ico i j) = Ioc j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioc i j) = Ico j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioo i j) = Ioo j.rev i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (uIcc i j) = uIcc i.rev j.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ici i) = Iic i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioi i) = Iio i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iic i) = Ici i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iio i) = Ioi i.rev

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ ↑k ≤ ↑(k - 1) ↔ k < k - 1

Tactic:
le_iff_lt_or_eq,

Goal state after:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ ↑k < ↑(k - 1) ∨ ↑k = ↑(k - 1) ↔ k < k - 1
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
have h₂ : map (Submodule.subtype (span R (range v))) (span R (range fun i => ⟨v i, this i⟩)) =
        span R (range v) := by
      rw [← span_image, Submodule.coe_subtype, h₁]

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
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✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
e : (linearCombination R Subtype.val) (embDomain u (b.repr x)) = ↑⟨x, p⟩
j : ι
W : b j = x
⊢ False

Tactic:
apply q ⟨j, W⟩

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

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x : R
i : ι
⊢ ((Basis.singleton ι R).repr x) i = x

Tactic:
simp [Basis.singleton, Unique.eq_default i]

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

Goal state before:
pp: case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

pp: case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
· simp only [one_epow, le_refl]

Goal state after:
case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤
Module: Mathlib.Algebra.Group.ModEq

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

Tactic:
rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]

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

Goal state before:
pp: 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)

Tactic:
← sub_eq_iff_eq_add

Goal state after:
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) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(chineseRemainder' h) < n.lcm m

Tactic:
dsimp only [chineseRemainder']
  rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]
  have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
  exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s).encard + s.encard = t.encard

Tactic:
← encard_union_eq disjoint_sdiff_left,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s ∪ s).encard = t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s \ t).encard + t.encard = (s ∪ t).encard

Tactic:
← encard_union_eq disjoint_sdiff_left,

Goal state after:
α : Type u_1
s t : Set α
⊢ (s \ t ∪ t).encard = (s ∪ t).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}

Tactic:
le_iff_lt_or_eq,

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ x, s = {x}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 2
x : α
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
← insert_eq_of_mem hx,

Goal state after:
α : Type u_1
s : Set α
x : α
h : (insert x s).encard = 2
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 3
x : α
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
← insert_eq_of_mem hx,

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : (insert x s).encard = 3
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 4
x : α
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
← insert_eq_of_mem hx,

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : (insert x s).encard = 4
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Module: Mathlib.Data.Set.Card

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

Tactic:
by
  rwa [ncard, ENat.natCast_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).ncard ≤ s.ncard

Tactic:
by
  to_encard_tac; rw [hs.cast_ncard_eq, (hs.image _).cast_ncard_eq]; apply encard_image_le

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
⊢ (fun i a ↦ a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)

Tactic:
obtain ⟨_, h⟩ := h i

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ (fun i a ↦ a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ φ (a⁻¹ * b) = 1

Tactic:
φ.map_mul,

Goal state after:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ φ a⁻¹ * φ b = 1
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
⊢ ∀ (a : ↥(H ⊔ N)), ∃ a_1, φ a_1 = Quotient.mk'' a

Tactic:
rintro ⟨y, hy : y ∈ (H ⊔ N)⟩

Goal state after:
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy : y ∈ H ⊔ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy⟩
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: α : Type u_4
M : Type u_5
inst✝² : MulOneClass M
inst✝¹ : SMul α M
inst✝ : IsScalarTower α M M
c : Con M
a : α
w x : M
h : c w x
⊢ c (a • w) (a • x)

Tactic:
by
  simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p ≤ (q.mkQ ∘ₛₗ f).ker

Tactic:
by simpa [ker_comp] using h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (pred a) b = Ico a b

Tactic:
Ioo_pred_left_eq_Ioc_of_not_isMin ha

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ico a b = Ico a b
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₂
⊢ IsCompl (inl R M M₂).range (inr R M M₂).range

Tactic:
constructor
  · rw [disjoint_def]
    rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩
    simp only [Prod.ext_iff, inl_apply, inr_apply] at hx hy ⊢
    exact ⟨hy.1.symm, hx.2.symm⟩
  · rw [codisjoint_iff_le_sup]
    rintro ⟨x, y⟩ -
    simp only [mem_sup, mem_range]
    refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩
    simp

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderBot α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
by
  simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', f.range = f'.graph

Tactic:
obtain ⟨f', hf'⟩ :=
    AddMonoidHom.exists_mrange_eq_mgraph (G := G) (H := H) (I := I) (f := f) hf₁ hf

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : AddMonoidHom.mrange ↑f = f'.mgraph
⊢ ∃ f', f.range = f'.graph
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) (Ioc a b) (Ioc (a + d) (b + d))

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]

Goal state after:
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) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
by_cases! h : m ≤ n
  · rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
  · replace h := h.le
    rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]

Goal state after: